Effective interactive proofs for higher-order imperative programs

ABSTRACT

We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. The verification burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. The core of the automation is a simplification procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-specific simplification rules.

We argue for the effectiveness of our infrastructure by verifying a number of data structures and a packrat parser, and we compare to similar efforts within other projects. Compared to competing approaches to data structure verification, our system includes much less code that must be trusted; namely, about a hundred lines of Coq code defining a program logic. All of our theorems and decision procedures have or build machine-checkable correctness proofs from first principles, removing opportunities for tool bugs to create faulty verifications.

REFERENCES

• 1: Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In Proc. CASSIS, 2004.
• 2: Bruno Barras and Bruno Bernardo. The Implicit Calculus of Constructions as a programming language with dependent types. In Proc. FoSSaCS, 2008.
• 3: Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Proc. FMCO, 2005.
• 4: Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer Verlag, 2004.
• 5: Bor-Yuh Evan Chang and Xavier Rival. Relational inductive shape analysis. In Proc. POPL, 2008.
• 6: Arthur Charguéraud and François Pottier. Functional translation of a calculus of capabilities. In Proc. ICFP, 2008.
• 7: Chiyan Chen and Hongwei Xi. Combining programming with theorem proving. In Proc. ICFP, 2005.
• 8: David Delahaye. A tactic language for the system Coq. In Proc. LPAR, 2000.
• 9: Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In Proc. PLDI, 2002.
• 10: Bryan Ford. Parsing expression grammars: A recognition-based syntactic foundation. In Proc. POPL, 2004.
• 11: Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. Sage: Hybrid checking for flexible specifications. In Proc. Scheme Workshop, 2006.
• 12: Matt Kaufmann and J. S. Moore. An industrial strength theorem prover for a logic based on Common Lisp. IEEE Trans. Softw. Eng., 23 (4), 1997.
• 13: Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proc. POPL, 2006.
• 14: Barbara Liskov and Stephen N. Zilles. Specification techniques for data abstractions. IEEE Trans. Software Eng., 1 (1): 7--19, 1975.
• 15: Conor McBride and James McKinna. The view from the left. J. Functional Programming, 14 (1): 69--111, 2004.
• 16: Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Polymorphism and separation in Hoare Type Theory. Proc. ICFP, 2006.
• 17: Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: Reasoning with the awkward squad. In Proc. ICFP, 2008.
• 18: Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007.
• 19: Emir Pasalic, Jeremy Siek, Walid Taha, and Seth Fogarty. Concoqtion: Indexed types now! In Proc. PEPM, 2007.
• 20: Lawrence C Paulson. Isabelle: A generic theorem prover. Journal of Automated Reasoning, 5, 1994.
• 21: Rasmus L. Petersen, Lars Birkedal, Aleksandar Nanevski, and Greg Morrisett. A realizability model for impredicative Hoare Type Theory. In Proc. ESOP, 2008.
• 22: John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. LICS, 2002.
• 23: Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. ACM TOPLAS, 24, 2002.
• 24: Wouter Swierstra and Thorsten Altenkirch. Beauty in the beast: A functional semantics for the awkward squad. In Proc. Haskell Workshop, 2007.
• 25: Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In Proc. PLDI, 2008.

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
          Subjects: Mechanical verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Reliability; Correctness proofs

General Terms:
Languages, Verification

Keywords:
dependent types, functional programming, interactive proof assistants, separation logic