• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

KIMURA Daisuke  木村 大輔

ORCIDConnect your ORCID iD *help
… Alternative Names

木村 大輔  キムラ ダイスケ

Less
Researcher Number 90455197
Other IDs
Affiliation (Current) 2025: 東邦大学, 理学部, 准教授
Affiliation (based on the past Project Information) *help 2022 – 2023: 東邦大学, 理学部, 准教授
2018 – 2023: 東邦大学, 理学部, 講師
2016: 東邦大学, 理学部情報科学科, 講師
Review Section/Research Field
Except Principal Investigator
Basic Section 60010:Theory of informatics-related / Basic Section 60050:Software-related / Theory of informatics
Keywords
Except Principal Investigator
分離論理 / ソフトウェア検証 / 帰納的述語 / カット除去 / 証明体系 / 不動点演算子 / カット除去可能性 / 循環証明体系 / メモリ安全性 / ソフトウェア解析 … More / 証明論 / シーケント計算 / 循環証明 / カット除去定理 / 数理論理 / 帰納的定義 / 記号ヒープ Less
  • Research Projects

    (4 results)
  • Research Products

    (15 results)
  • Co-Researchers

    (2 People)
  •  循環証明体系におけるカット除去定理とカット規則の制限

    • Principal Investigator
      中澤 巧爾
    • Project Period (FY)
      2022 – 2025
    • Research Category
      Grant-in-Aid for Scientific Research (C)
    • Review Section
      Basic Section 60010:Theory of informatics-related
    • Research Institution
      Nagoya University
  •  分離論理を用いたソフトウェア検証の発展

    • Principal Investigator
      龍田 真
    • Project Period (FY)
      2021 – 2023
    • Research Category
      Grant-in-Aid for Scientific Research (B)
    • Review Section
      Basic Section 60050:Software-related
    • Research Institution
      National Institute of Informatics
  •  Proof theoretic analysis of cyclic proof systems

    • Principal Investigator
      Nakazawa Koji
    • Project Period (FY)
      2018 – 2020
    • Research Category
      Grant-in-Aid for Scientific Research (C)
    • Review Section
      Basic Section 60010:Theory of informatics-related
    • Research Institution
      Nagoya University
  •  Theory of software verification by separation logic

    • Principal Investigator
      Tatsuta Makoto
    • Project Period (FY)
      2015 – 2016
    • Research Category
      Grant-in-Aid for Scientific Research (C)
    • Research Field
      Theory of informatics
    • Research Institution
      National Institute of Informatics

All 2022 2021 2020 2019 2016 2015

All Journal Article Presentation

  • [Journal Article] Cut-elimination for cyclic proof systems with inductively defined propositions2022

    • Author(s)
      Daisuke Kimura, Koji Nakazawa, and Kenji Saotome
    • Journal Title

      RIMS Kokyuroku

      Volume: 2228 Pages: 30-40

    • Open Access
    • Data Source
      KAKENHI-PROJECT-22K11901
  • [Journal Article] Biabduction for Separation Logic with Arrays and Lists2022

    • Author(s)
      Daisuke Kimura, Makoto Tatsuta, Mahmudul Faisal Al Ameen, oji Nakazawa, and Mirai Ikebuchi
    • Journal Title

      Biabduction for Separation Logic with Arrays and Lists

      Volume: 1

    • Peer Reviewed / Int'l Joint Research
    • Data Source
      KAKENHI-PROJECT-21H03421
  • [Journal Article] Function Pointer Eliminator for C Programs2021

    • Author(s)
      Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, and Koji Nakazawa
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 13008 Pages: 23-37

    • DOI

      10.1007/978-3-030-89051-3_2

    • ISBN
      9783030890506, 9783030890513
    • Peer Reviewed / Int'l Joint Research
    • Data Source
      KAKENHI-PROJECT-18H03226, KAKENHI-PROJECT-21H03421
  • [Journal Article] Decidability for Entailments of Symbolic Heaps with Arrays2021

    • Author(s)
      Daisuke Kimura, Makoto Tatsuta
    • Journal Title

      Logical Methods in Computer Science

      Volume: 17 (2)

    • Peer Reviewed
    • Data Source
      KAKENHI-PROJECT-21H03421
  • [Journal Article] Restriction on Cut in Cyclic Proof System for Symbolic Heaps2020

    • Author(s)
      Saotome Kenji、Nakazawa Koji、Kimura Daisuke
    • Journal Title

      FLOPS 2020, Lecture Notes in Computer Science

      Volume: 12073 Pages: 88-105

    • DOI

      10.1007/978-3-030-59025-3_6

    • ISBN
      9783030590246, 9783030590253
    • Peer Reviewed
    • Data Source
      KAKENHI-PROJECT-18K11161
  • [Journal Article] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2020

    • Author(s)
      KIMURA Daisuke、NAKAZAWA Koji、TERAUCHI Tachio、UNNO Hiroshi
    • Journal Title

      Computer Software

      Volume: 37 Issue: 1 Pages: 1_39-1_52

    • DOI

      10.11309/jssst.37.1_39

    • NAID

      130007815024

    • ISSN
      0289-6540
    • Year and Date
      2020-01-24
    • Language
      Japanese
    • Peer Reviewed / Open Access
    • Data Source
      KAKENHI-PROJECT-18K11161, KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-17H01723
  • [Journal Article] Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions2019

    • Author(s)
      Tatsuta Makoto、Nakazawa Koji、Kimura Daisuke
    • Journal Title

      LNCS (APLAS 2019)

      Volume: 11893 Pages: 367-387

    • DOI

      10.1007/978-3-030-34175-6_19

    • ISBN
      9783030341749, 9783030341756
    • Peer Reviewed
    • Data Source
      KAKENHI-PROJECT-18K11161, KAKENHI-PROJECT-17H01722
  • [Journal Article] Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic2016

    • Author(s)
      Makoto Tatsuta and Daisuke Kimura
    • Journal Title

      Proceedings of the 18th JSSST Workshop on Programming and Programming Languages

      Volume: 1

    • Peer Reviewed
    • Data Source
      KAKENHI-PROJECT-15K00027
  • [Journal Article] Separation Logic with Monadic Inductive Definitions and Implicit Existentials2015

    • Author(s)
      Makoto Tatsuta and Daisuke Kimura
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 9458

    • Peer Reviewed
    • Data Source
      KAKENHI-PROJECT-15K00027
  • [Presentation] 分離論理における記号ヒープのための循環証明体系におけるカットの制限について2020

    • Author(s)
      早乙女献自,中澤巧爾,木村大輔
    • Organizer
      第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)
    • Data Source
      KAKENHI-PROJECT-18K11161
  • [Presentation] Failure of cut-elimination in cyclic proofs of separation logic2019

    • Author(s)
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno
    • Organizer
      第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
    • Data Source
      KAKENHI-PROJECT-18K11161
  • [Presentation] On cut elimination in cyclic-proof systems2019

    • Author(s)
      Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, and Kenji Saotome
    • Organizer
      3rd Workshop on Mathamatical Logic and Its Applications (MLA 2019)
    • Int'l Joint Research
    • Data Source
      KAKENHI-PROJECT-18K11161
  • [Presentation] Spatial factorization in cyclic-proof system for separation logic2019

    • Author(s)
      Koji Nakazawa, Makoto Tatsuta, and Daisuke Kimura
    • Organizer
      第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
    • Data Source
      KAKENHI-PROJECT-18K11161
  • [Presentation] Decidability of Entailments in Separation Logic with Arrays2016

    • Author(s)
      Daisuke Kimura
    • Organizer
      Workshop on Mathematical Logic and its Application
    • Place of Presentation
      京都大学
    • Year and Date
      2016-09-16
    • Int'l Joint Research
    • Data Source
      KAKENHI-PROJECT-15K00027
  • [Presentation] Decidability and Undecidability in Symbolic-Heap System with Inductive Definitions2015

    • Author(s)
      Makoto Tatsuta and Daisuke Kimura
    • Organizer
      Continuity, Computability, Constructivity: From Logic to Algorithms (CCC2015)
    • Place of Presentation
      Kochel, Germany
    • Year and Date
      2015-09-16
    • Int'l Joint Research
    • Data Source
      KAKENHI-PROJECT-15K00027
  • 1.  Nakazawa Koji (80362581)
    # of Collaborated Projects: 3 results
    # of Collaborated Products: 8 results
  • 2.  Tatsuta Makoto (80216994)
    # of Collaborated Projects: 2 results
    # of Collaborated Products: 6 results

URL: 

Are you sure that you want to link your ORCID iD to your KAKEN Researcher profile?
* This action can be performed only by the researcher himself/herself who is listed on the KAKEN Researcher’s page. Are you sure that this KAKEN Researcher’s page is your page?

この研究者とORCID iDの連携を行いますか?
※ この処理は、研究者本人だけが実行できます。

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi