Advertisement

Automated mutual induction proof in separation logic

  • Quang-Trung Ta
  • Ton Chanh Le
  • Siau-Cheng Khoo
  • Wei-Ngan Chin
Original Article

Abstract

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.

Keywords

Separation logic Entailment proving Mathematical induction Mutual induction 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Notes

Acknowledgements

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.

References

  1. BCI11.
    Berdine J, Cook B, Ishtiaq S (2011) SLAyer: memory safety for systems-level code. In: International conference on computer aided verification (CAV), pp 178–183CrossRefGoogle Scholar
  2. BCO04.
    Berdine J, Calcagno C, O'Hearn PW (2004) A decidable fragment of separation logic. In: International conference on foundations of software technology and theoretical computer science (FSTTCS), pp 97–109CrossRefGoogle Scholar
  3. BCO05.
    Berdine J, Calcagno C, O'Hearn PW (2005) Symbolic execution with separation logic. In: Asian symposium on programming languages and systems (APLAS), pp 52–68CrossRefGoogle Scholar
  4. BDP11.
    Brotherston J, Distefano D, Petersen RL (2011) Automated cyclic entailment proofs in separation logic. In: International conference on automated deduction (CADE), pp 131–146zbMATHGoogle Scholar
  5. BGP12.
    Brotherston J, Gorogiannis N, Petersen RL (2012) A generic cyclic theorem prover. In: Asian symposium on programming languages and systems (APLAS), pp 350–367CrossRefGoogle Scholar
  6. BIP10.
    Bozga, M., Iosif, R., Perarnau, S.: Quantitative separation logic and programs with lists. J Autom Reason 45(2), 131–156 (2010)MathSciNetCrossRefGoogle Scholar
  7. 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
  8. Bro07.
    Brotherston J (2007) Formalised inductive reasoning in the logic of bunched implications. In: International static analysis symposium (SAS), pp 87–103Google Scholar
  9. Bun01.
    Bundy, A (2001) The automation of proof by mathematical induction. In: Robinson, JA, Voronkov, A (eds) Handbook of automated reasoning, vol 2. Elsevier, MIT Press, pp 845–911CrossRefGoogle Scholar
  10. 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
  11. Chi+12.
    Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci Comput Program 77(9), 1006–1036 (2012)CrossRefGoogle Scholar
  12. 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
  13. 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
  14. ESW15.
    Enea C, Sighireanu M, Wu Z (2015) On automated lemma generation for separation logic with inductive definitions. In: International symposium on automated technology for verification and analysis (ATVA), pp 80–96CrossRefGoogle Scholar
  15. God92.
    Godel K (1992) On formally undecidable propositions of principia mathematica and related systems (Meltzer B, Trans.). Dover Publications, Mineola. ISBN: 0486669807Google Scholar
  16. Har09.
    Harrison J (2009) Handbook of practical logic and automated reasoning, 1st edn. Cambridge University Press, New York. ISBN: 0521899575, 9780521899574Google Scholar
  17. IRS13.
    Iosif R, Rogalewicz A, Simácek J (2013) The tree width of separation logic with recursive definitions. In: International conference on automated deduction (CADE), pp 21–38CrossRefGoogle Scholar
  18. 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
  19. KN87.
    Kapur, D., Narendran, P.: Matching, unification and complexity. ACM SIGSAM Bull 21(4), 6–9 (1987)CrossRefGoogle Scholar
  20. 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
  21. 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
  22. 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
  23. 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
  24. 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
  25. PR13.
    Pérez JAN, Rybalchenko A (2013) Separation logic modulo theories. In: Asian symposium on programming languages and systems (APLAS), pp 90–106Google Scholar
  26. PWZ13.
    Piskac R, Wies T, Zufferey D (2013) Automating separation logic using SMT. In: International conference on computer aided verification (CAV), pp 773–789CrossRefGoogle Scholar
  27. 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
  28. 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
  29. 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
  30. SC16.
    Sighireanu, M., Cok, D.R.: Report on SL-COMP 2014. J Satisf Boolean Model Comput 9, 173–186 (2016)MathSciNetGoogle Scholar
  31. 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
  32. Ta+18.
    Ta Q-T, Le TC, Khoo S-C, Chin W-N (2018) Automated lemma synthesis in symbolic-heap separation logic. In: Symposium on principles of programming languages (POPL), pp 9:1–9:29CrossRefGoogle Scholar

Copyright information

© British Computer Society 2018

Authors and Affiliations

  • Quang-Trung Ta
    • 1
  • Ton Chanh Le
    • 2
  • Siau-Cheng Khoo
    • 1
  • Wei-Ngan Chin
    • 1
  1. 1.Department of Computer Science, School of ComputingNational University of SingaporeSingaporeSingapore
  2. 2.Department of Computer ScienceStevens Institute of TechnologyHobokenUSA

Personalised recommendations