木村大輔 KIMURA Daisuke

研究者番号	90455197
その他のID
所属 (現在)	2025年度: 東邦大学, 理学部, 准教授
所属 (過去の研究課題情報に基づく) *注記	2022年度 – 2023年度: 東邦大学, 理学部, 准教授 2018年度 – 2023年度: 東邦大学, 理学部, 講師 2016年度: 東邦大学, 理学部情報科学科, 講師
審査区分/研究分野	研究代表者以外小区分60010:情報学基礎論関連 / 小区分60050:ソフトウェア関連 / 情報学基礎理論
キーワード	研究代表者以外分離論理 / ソフトウェア検証 / 帰納的述語 / カット除去 / 証明体系 / 不動点演算子 / カット除去可能性 / 循環証明体系 / メモリ安全性 / ソフトウェア解析 … もっと見る / 証明論 / シーケント計算 / 循環証明 / カット除去定理 / 数理論理 / 帰納的定義 / 記号ヒープ隠す

循環証明体系におけるカット除去定理とカット規則の制限
- 研究代表者
  
  中澤巧爾
- 研究期間 (年度)
  2022 – 2025
- 研究種目
  
  基盤研究(C)
- 審査区分
  
  小区分60010:情報学基礎論関連
- 研究機関
  名古屋大学
分離論理を用いたソフトウェア検証の発展
- 研究代表者
  
  龍田真
- 研究期間 (年度)
  2021 – 2023
- 研究種目
  
  基盤研究(B)
- 審査区分
  
  小区分60050:ソフトウェア関連
- 研究機関
  国立情報学研究所
循環証明体系の証明論的分析
- 研究代表者
  
  中澤巧爾
- 研究期間 (年度)
  2018 – 2020
- 研究種目
  
  基盤研究(C)
- 審査区分
  
  小区分60010:情報学基礎論関連
- 研究機関
  名古屋大学
分離論理を用いたソフトウェア検証の基礎理論
- 研究代表者
  
  龍田真
- 研究期間 (年度)
  2015 – 2016
- 研究種目
  
  基盤研究(C)
- 研究分野
  
  情報学基礎理論
- 研究機関
  国立情報学研究所

すべて 2022 2021 2020 2019 2016 2015

すべて雑誌論文学会発表

[雑誌論文] Cut-elimination for cyclic proof systems with inductively defined propositions2022
- 著者名/発表者名
  Daisuke Kimura, Koji Nakazawa, and Kenji Saotome
- 雑誌名
  
  RIMS Kokyuroku
  
  巻: 2228 ページ: 30-40
- オープンアクセス
- データソース
  KAKENHI-PROJECT-22K11901
[雑誌論文] Biabduction for Separation Logic with Arrays and Lists2022
- 著者名/発表者名
  Daisuke Kimura, Makoto Tatsuta, Mahmudul Faisal Al Ameen, oji Nakazawa, and Mirai Ikebuchi
- 雑誌名
  
  Biabduction for Separation Logic with Arrays and Lists
  
  巻: 1
- 査読あり / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-21H03421
[雑誌論文] Function Pointer Eliminator for C Programs2021
- 著者名/発表者名
  Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, and Koji Nakazawa
- 雑誌名
  
  Lecture Notes in Computer Science
  
  巻: 13008 ページ: 23-37
- DOI
  10.1007/978-3-030-89051-3_2
- ISBN
  9783030890506, 9783030890513
- 査読あり / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-18H03226, KAKENHI-PROJECT-21H03421
[雑誌論文] Decidability for Entailments of Symbolic Heaps with Arrays2021
- 著者名/発表者名
  Daisuke Kimura, Makoto Tatsuta
- 雑誌名
  
  Logical Methods in Computer Science
  
  巻: 17 (2)
- 査読あり
- データソース
  KAKENHI-PROJECT-21H03421
[雑誌論文] Restriction on Cut in Cyclic Proof System for Symbolic Heaps2020
- 著者名/発表者名
  Saotome Kenji、Nakazawa Koji、Kimura Daisuke
- 雑誌名
  
  FLOPS 2020, Lecture Notes in Computer Science
  
  巻: 12073 ページ: 88-105
- DOI
  10.1007/978-3-030-59025-3_6
- ISBN
  9783030590246, 9783030590253
- 査読あり
- データソース
  KAKENHI-PROJECT-18K11161
[雑誌論文] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2020
- 著者名/発表者名
  KIMURA Daisuke、NAKAZAWA Koji、TERAUCHI Tachio、UNNO Hiroshi
- 雑誌名
  
  コンピュータソフトウェア
  
  巻: 37 号: 1 ページ: 1_39-1_52
- DOI
  10.11309/jssst.37.1_39
- NAID
  130007815024
- ISSN
  0289-6540
- 年月日
  2020-01-24
- 言語
  日本語
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-18K11161, KAKENHI-PROJECT-18K19787, KAKENHI-PROJECT-17H01720, KAKENHI-PROJECT-17H01723
[雑誌論文] Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions2019
- 著者名/発表者名
  Tatsuta Makoto、Nakazawa Koji、Kimura Daisuke
- 雑誌名
  
  LNCS (APLAS 2019)
  
  巻: 11893 ページ: 367-387
- DOI
  10.1007/978-3-030-34175-6_19
- ISBN
  9783030341749, 9783030341756
- 査読あり
- データソース
  KAKENHI-PROJECT-18K11161, KAKENHI-PROJECT-17H01722
[雑誌論文] Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic2016
- 著者名/発表者名
  Makoto Tatsuta and Daisuke Kimura
- 雑誌名
  
  Proceedings of the 18th JSSST Workshop on Programming and Programming Languages
  
  巻: 1
- 査読あり
- データソース
  KAKENHI-PROJECT-15K00027
[雑誌論文] Separation Logic with Monadic Inductive Definitions and Implicit Existentials2015
- 著者名/発表者名
  Makoto Tatsuta and Daisuke Kimura
- 雑誌名
  
  Lecture Notes in Computer Science
  
  巻: 9458
- 査読あり
- データソース
  KAKENHI-PROJECT-15K00027
[学会発表] 分離論理における記号ヒープのための循環証明体系におけるカットの制限について2020
- 著者名/発表者名
  早乙女献自，中澤巧爾，木村大輔
- 学会等名
  第22回プログラミングおよびプログラミング言語ワークショップ(PPL2020)
- データソース
  KAKENHI-PROJECT-18K11161
[学会発表] Failure of cut-elimination in cyclic proofs of separation logic2019
- 著者名/発表者名
  Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, and Hiroshi Unno
- 学会等名
  第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
- データソース
  KAKENHI-PROJECT-18K11161
[学会発表] On cut elimination in cyclic-proof systems2019
- 著者名/発表者名
  Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, and Kenji Saotome
- 学会等名
  3rd Workshop on Mathamatical Logic and Its Applications (MLA 2019)
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-18K11161
[学会発表] Spatial factorization in cyclic-proof system for separation logic2019
- 著者名/発表者名
  Koji Nakazawa, Makoto Tatsuta, and Daisuke Kimura
- 学会等名
  第21回プログラミングおよびプログラミング言語ワークショップ (PPL2019)
- データソース
  KAKENHI-PROJECT-18K11161
[学会発表] Decidability of Entailments in Separation Logic with Arrays2016
- 著者名/発表者名
  Daisuke Kimura
- 学会等名
  Workshop on Mathematical Logic and its Application
- 発表場所
  京都大学
- 年月日
  2016-09-16
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15K00027
[学会発表] Decidability and Undecidability in Symbolic-Heap System with Inductive Definitions2015
- 著者名/発表者名
  Makoto Tatsuta and Daisuke Kimura
- 学会等名
  Continuity, Computability, Constructivity: From Logic to Algorithms (CCC2015)
- 発表場所
  Kochel, Germany
- 年月日
  2015-09-16
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-15K00027

1. 中澤巧爾 (80362581)

共同の研究課題数: 3件

共同の研究成果数: 8件
2. 龍田真 (80216994)

共同の研究課題数: 2件

共同の研究成果数: 6件

木村 大輔 KIMURA Daisuke

研究課題

研究成果

共同研究者

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

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

分離論理を用いたソフトウェア検証の発展

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

循環証明体系の証明論的分析

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

分離論理を用いたソフトウェア検証の基礎理論

研究代表者

研究期間 (年度)

研究種目

研究分野

研究機関

[雑誌論文] Cut-elimination for cyclic proof systems with inductively defined propositions2022

著者名/発表者名

雑誌名

データソース

[雑誌論文] Biabduction for Separation Logic with Arrays and Lists2022

著者名/発表者名

雑誌名

データソース

[雑誌論文] Function Pointer Eliminator for C Programs2021

著者名/発表者名

雑誌名

DOI

ISBN

データソース

[雑誌論文] Decidability for Entailments of Symbolic Heaps with Arrays2021

著者名/発表者名

雑誌名

データソース

[雑誌論文] Restriction on Cut in Cyclic Proof System for Symbolic Heaps2020

著者名/発表者名

雑誌名

DOI

ISBN

データソース

[雑誌論文] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2020

著者名/発表者名

雑誌名

DOI

NAID

ISSN

年月日

言語

データソース

[雑誌論文] Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions2019

著者名/発表者名

雑誌名

DOI

ISBN

データソース

[雑誌論文] Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic2016

著者名/発表者名

雑誌名

データソース

[雑誌論文] Separation Logic with Monadic Inductive Definitions and Implicit Existentials2015

著者名/発表者名

雑誌名

データソース

[学会発表] 分離論理における記号ヒープのための循環証明体系におけるカットの制限について2020

著者名/発表者名

学会等名

データソース

[学会発表] Failure of cut-elimination in cyclic proofs of separation logic2019

木村大輔 KIMURA Daisuke