Theory of software verification by separation logic

2016 Fiscal Year Final Research Report

• Project/Area Number: 15K00027
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Theory of informatics
• Research Institution: National Institute of Informatics
• Principal Investigator: Tatsuta Makoto 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
• Co-Investigator(Renkei-kenkyūsha): KIMURA Daisuke 東邦大学, 理学部情報科学科, 講師 (90455197)
• Project Period (FY): 2015-04-01 – 2017-03-31
• Keywords: 分離論理 / ソフトウェア検証 / 記号ヒープ / 帰納的定義

Outline of Final Research Achievements

(1) We proved the decidability of entailments in separation logic with monadic inductive definitions and implicit existentials. This system is obtained from the bounded-treewidth separation logic SLRDbtw by adding implicit existential variables and restricting inductive definitions to monadic ones. (2) We implemented an entailment checker for the logical system of symbolic heaps with monadic inductive definitions. We proposed optimization of equivalence relation on tree nodes. for efficient implementation. (3) We proved the completeness of an extension of Hoare's logic and separation logic for pointer programs with mutual recursive procedures. (4) For the satisfiability problem of symbolic heaps in separation logic with Presburger arithmetic and inductive definitions. we first proved the system without any restrictions is undecidable. Secondly we proposed some syntactic restrictions and we proved the decidability by presenting a decision procedure.

Free Research Field

理論計算機科学および数理論理学