Theory of software verification by separation logic

分离逻辑的软件验证理论

• 批准号: 15K00027
• 负责人: Tatsuta Makoto
• 金额: $ 3万
• 依托单位: National Institute of Informatics
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2015
• 资助国家: 日本
• 起止时间: 2015-04-01 至 2017-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15K00027/
• 关键词: 分離論理; ソフトウェア検証; 記号ヒープ; 帰納的定義; 数理論理

项目成果

Separation Logic with Monadic Inductive Definitions and Implicit Existentials

具有一元归纳定义和隐式存在的分离逻辑

• 发表时间: 2015
• 期刊: Lecture Notes in Computer Science
• 作者: Makoto Tatsuta and Daisuke Kimura

Decidability of Entailments in Separation Logic with Arrays

数组分离逻辑中蕴涵的可判定性

• 发表时间: 2016
• 作者: 永嶋裕樹;白柳潔;Daisuke Kimura
• 通讯作者: Daisuke Kimura

Completeness for Recursive Procedures in Separation Logic

分离逻辑中递归过程的完整性

• DOI: 10.1016/j.tcs.2016.04.004
• 发表时间: 2016
• 期刊: Theoretical Computer Science
• 影响因子: 1.1
• 作者: 櫻井優太;関川浩;Mahmudul Faisal Al Ameen and Makoto Tatsuta
• 通讯作者: Mahmudul Faisal Al Ameen and Makoto Tatsuta

Decidability and Undecidability in Symbolic-Heap System with Inductive Definitions

具有归纳定义的符号堆系统中的可判定性和不可判定性

• 发表时间: 2015
• 作者: Akiyuki Katayama;Kiyoshi Shirayanagi;Makoto Tatsuta and Daisuke Kimura
• 通讯作者: Makoto Tatsuta and Daisuke Kimura

Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic

将具有一元归纳定义的符号堆转换为一元二阶逻辑

• 发表时间: 2016
• 期刊: Proceedings of the 18th JSSST Workshop on Programming and Programming Languages
• 作者: 片山彰之;白柳潔;Makoto Tatsuta and Daisuke Kimura
• 通讯作者: Makoto Tatsuta and Daisuke Kimura