Automated mutual induction proof in separation logic
We present a deductive proof system to automatically prove separation logic entailments by mathematical induction. Our technique is called the mutual induction proof. It is an instance of the well-founded induction, a.k.a., Noetherian induction. More specifically, we propose a novel induction principle based on a well-founded relation of separation logic models. We implement this principle explicitly as inference rules so that it can be easily integrated into a deductive proof system. Our induction principle allows a goal entailment and other entailments derived during the proof search to be used as hypotheses to mutually prove each other. This feature increases the success chance of proving the goal entailment. We have implemented this mutual induction proof technique in a prototype prover and evaluated it on two entailment benchmarks collected from the literature as well as a synthetic benchmark. The experimental results are promising since our prover can prove most of the valid entailments in these benchmarks, and achieves a better performance than other state-of-the-art separation logic provers.
KeywordsSeparation logic Entailment proving Mathematical induction Mutual induction
Unable to display preview. Download preview PDF.
We would like to thank the anonymous reviewers of the Formal Aspect of Computing journal for the careful reading and the constructive comments on our work. The first author wishes to thank Dr. Alwen Fernanto Tiu and an anonymous reviewer of LICS 2018 for the suggestion of using the term matching, instead of the term unification, when describing the induction hypothesis application. This research is partially supported by an NUS research Grant R-252-000-553-112 and an MoE Tier-2 Grant MOE2013-T2-2-146.
- Bro+16.Brotherston J, Gorogiannis N, Kanovich MI, Rowe R (2016) Model checking for Symbolic-Heap Separation Logic with inductive predicates. In: Symposium on principles of programming languages (POPL), pp 84–96Google Scholar
- Bro07.Brotherston J (2007) Formalised inductive reasoning in the logic of bunched implications. In: International static analysis symposium (SAS), pp 87–103Google Scholar
- Cal+15.Calcagno C, Distefano D, Dubreil J, Gabi D, Hooimeijer P, Luca M, O'Hearn PW, Papakonstantinou I, Purbrick J, Rodriguez D (2015) Moving fast with software verification. In: NASA international symposium on formal methods (NFM), pp 3–11Google Scholar
- CJT15.Chu D-H, Jaffar J, Trinh M-T (2015) Automatic induction proofs of data-structures in imperative programs. In: Conference on programming language design and implementation (PLDI), pp 457–466Google Scholar
- Ene+14.Enea C, Lengál O, Sighireanu M, Vojnar T (2014) Compositional entailment checking for a fragment of separation logic. In: Asian symposium on programming languages and systems (APLAS), pp 314–333Google Scholar
- God92.Godel K (1992) On formally undecidable propositions of principia mathematica and related systems (Meltzer B, Trans.). Dover Publications, Mineola. ISBN: 0486669807Google Scholar
- Har09.Harrison J (2009) Handbook of practical logic and automated reasoning, 1st edn. Cambridge University Press, New York. ISBN: 0521899575, 9780521899574Google Scholar
- IRV14.Iosif R, Rogalewicz A, Vojnar T (2014) Deciding entailments in inductive separation logic with tree automata. In: International symposium on automated technology for verification and analysis (ATVA), pp 201–218Google Scholar
- MB08.De Moura LM, Bjørner N (2008) Z3: an efficient SMT solver. In: International conference on tools and algorithms for construction and analysis of systems (TACAS), pp 337–340Google Scholar
- NC08.Nguyen HH, Chin W-N (Wei-Ngan) Enhancing program verification with lemmas. In: International conference on computer aided verification (CAV), pp 355–369Google Scholar
- Ngu+07.Nguyen HH, David C, Qin S, Chin W-N (2007) Automated verification of shape and size properties via separation logic. In: International conference on verification, model checking, and abstract interpretation (VMCAI), pp 251–266Google Scholar
- PQM14.Pek E, Qiu X, Madhusudan P (2014) Natural proofs for data structure manipulation in C using separation logic. In: Conference on programming language design and implementation (PLDI), p 46Google Scholar
- PR11.Pérez JAN, Rybalchenko A (2011) Separation Logic + superposition calculus = heap theorem prover. In: Conference on programming language design and implementation (PLDI), pp 556–566Google Scholar
- PR13.Pérez JAN, Rybalchenko A (2013) Separation logic modulo theories. In: Asian symposium on programming languages and systems (APLAS), pp 90–106Google Scholar
- Qiu+13.Qiu X, Garg P, Stefanescu A, Madhusudan P (2013) Natural proofs for structure, data, and separation. In: Conference on programming language design and implementation (PLDI), pp 231–242Google Scholar
- Rey02.Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Symposium on logic in computer science (LICS), pp 55–74Google Scholar
- Rey08.Reynolds JC (2008) An introduction to separation logic. In: Lecture notes for the PhD fall school on logics and semantics of state, Copenhagen. Retrieved on 2017, March 16th, 2008. http://www.cs.cmu.edu/~jcr/copenhagen08.pdf
- Ta+16.Ta Q-T, Le TC, Khoo S-C, Chin W-N (2016) Automated mutual explicit induction proof in separation logic. In: FM 2016: Formal methods—21st international symposium, Limassol, Cyprus, 9–11 Nov 2016, Proceedings. pp 659–676Google Scholar