Cyclic proofs of program termination in separation logic

ABSTRACT

We propose a novel approach to proving the termination of heap-manipulating programs, which combines separation logic with cyclic proof within a Hoare-style proof system.Judgements in this system express (guaranteed) termination of the program when started from a given line in the program and in a state satisfying a given precondition, which is expressed as a formula of separation logic. The proof rules of our system are of two types: logical rules that operate on preconditions; and symbolic execution rules that capture the effect of executing program commands.

Our logical preconditions employ inductively defined predicates to describe heap properties, and proofs in our system are cyclic proofs: cyclic derivations in which some inductive predicate is unfolded infinitely often along every infinite path, thus allowing us to discard all infinite paths in the proof by an infinite descent argument. Moreover, the use of this soundness condition enables us to avoid the explicit construction and use of ranking functions for termination. We also give a completeness result for our system, which is relative in that it relies upon completeness of a proof system for logical implications in separation logic. We give examples illustrating our approach, including one example for which thecorresponding ranking function is non-obvious: termination of the classical algorithm for in-place reversal of a (possibly cyclic) linked list.

REFERENCES

• 1: Peter Aczel. An introduction to inductive definitions. In Jon Barwise, editor, Handbook of Mathematical Logic, pages 739--782. N-H, 1977.
• 2: Amir M. Ben-Amram and Chin Soon Lee. Ranking functions for size change termination II. Presented at (Hofbauer and Serebrenik 2007), 2007.
• 3: J. Berdine, C. Calcagno, and P.W. O'Hearn. Symbolic execution with separation logic. In APLAS 2005, volume 3780 of LNCS, pages 52--68, 2005.
• 4: J. Berdine, C. Calcagno, and P.W. O'Hearn. Smallfoot: Automatic modular assertion checking with separation logic. In FMCO, volume 4111 of LNCS, pages 115--137, 2006a.
• 5: J. Berdine, B. Cook, D. Distefano, and P. O'Hearn. Automatic termination proofs for programs with shape-shifting heaps. In CAV, volume 4144 of LNCS, pages 386--400, 2006b.
• 6: Josh Berdine , Aziem Chawdhary , Byron Cook , Dino Distefano , Peter O'Hearn, Variance analyses from invariance analyses, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 7: Richard Bornat, Cristiano Calcagno, and Peter O'Hearn. Local reasoning, separation and aliasing. In SPACE Workshop, 2004.
• 8: James Brotherston. Cyclic proofs for first-order logic with inductive definitions. In B. Beckert, editor, TABLEAUX 2005, volume 3702 of LNAI, pages 78--92. Springer-Verlag, 2005.
• 9: James Brotherston. Formalised inductive reasoning in the logic of bunched implications. In SAS-14, volume 4634 of LNCS, pages 87--103. Springer-Verlag, August 2007.
• 10: James Brotherston. Sequent Calculus Proof Systems for Inductive Definitions. PhD thesis, University of Edinburgh, November 2006.
• 11: James Brotherston , Alex Simpson, Complete Sequent Calculi for Induction and Infinite Descent, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.51-62, July 10-14, 2007 [doi>10.1109/LICS.2007.16]
• 12: C. Calcagno, D. Distefano, P.W. O'Hearn, and H. Yang. Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In SAS, volume 4134 of LNCS, pages 182--203, 2006.
• 13: D. Distefano, P. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS, volume 3920 of LNCS, pages 287--302, 2006.
• 14: Bolei Guo , Neil Vachharajani , David I. August, Shape analysis with inductive recursion synthesis, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 15: Dieter Hofbauer and Alexander Serebrenik. The 9th international workshop on termination. Paris, France, 2007.
• 16: Chin Soon Lee , Neil D. Jones , Amir M. Ben-Amram, The size-change principle for program termination, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-92, January 2001, London, United Kingdom
• 17: O. Lee, H. Yang, and K. Yi. Automatic verification of pointer programs using grammar-based shape analysis. In ESOP, volume 3444 of LNCS, pages 124--140, 2005.
• 18: Per Martin-Löf. Haupstatz for the intuitionistic theory of iterated inductive definitions. In J.E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 179--216. N-H, 1971.
• 19: P. W. O'Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215--244, June 99.
• 20: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 21: Byron Cook , Andreas Podelski , Andrey Rybalchenko, Termination proofs for systems code, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 22: Ulrich Schöpp , Alex K. Simpson, Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processes, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, p.372-386, April 08-12, 2002
• 23: Christoph Sprenger and Mads Dam. On the structure of inductive reasoning: circular and tree-shaped proofs in the μ-calculus. In FOSSACS 2003, volume 2620 of LNCS, pages 425--440, 2003.
• 24: Lars Birkedal , Noah Torp-Smith , John C. Reynolds, Local reasoning about a copying garbage collector, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.220-231, January 14-16, 2004, Venice, Italy
• 25: Hongseok Yang , Peter W. O'Hearn, A Semantic Basis for Local Reasoning, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, p.402-416, April 08-12, 2002

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Reliability, Theory, Verification

Keywords:
cyclic proof, hoare logic, inductive definitions, program verification, separation logic, termination