Theory of software verification by separation logic

• 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
• Project Status: Completed (Fiscal Year 2016)
• Budget Amount: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000); Fiscal Year 2017: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000); Fiscal Year 2016: ¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000); Fiscal Year 2015: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
• 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.

Research Products

• [Journal Article] Completeness for Recursive Procedures in Separation Logic (2016)
  • Author(s): Mahmudul Faisal Al Ameen and Makoto Tatsuta
  • Journal Title: Theoretical Computer Science Volume: 631 Pages: 73-96
  • DOI: 10.1016/j.tcs.2016.04.004
  • Peer Reviewed
• [Journal Article] Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic (2016)
  • Author(s): Makoto Tatsuta, Quang Loc Le, and Wei-Ngan Chin
  • Journal Title: Lecture Notes in Computer Science Volume: 10017 Pages: 423-443
  • DOI: 10.1007/978-3-319-47958-3_22
  • ISBN: 9783319479576, 9783319479583
  • Peer Reviewed
• [Journal Article] Translation of Symbolic Heaps with Monadic Inductive Definitions into Monadic Second-Order Logic (2016)
  • Author(s): Makoto Tatsuta and Daisuke Kimura
  • Journal Title: Proceedings of the 18th JSSST Workshop on Programming and Programming Languages Volume: 1
  • Peer Reviewed
• [Journal Article] Separation Logic with Monadic Inductive Definitions and Implicit Existentials (2015)
  • Author(s): Makoto Tatsuta and Daisuke Kimura
  • Journal Title: Lecture Notes in Computer Science Volume: 9458
  • Peer Reviewed
• [Presentation] Decidability of Entailments in Separation Logic with Arrays (2016)
  • 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
• [Presentation] Decidable subsystem of Presburger Arithmetic with Inductive Definitions and Application to Symbolic Heaps (2016)
  • Author(s): Makoto Tatsuta
  • Organizer: International Workshop on Mathematics for Computation (M4C)
  • Place of Presentation: Niederalteich, Germany
  • Year and Date: 2016-05-08
  • Int'l Joint Research
• [Presentation] Decidability and Undecidability in Symbolic-Heap System with Inductive Definitions (2015)
  • 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