Adam Chlipala
Gregory Malecha
Greg Morrisett
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.
Supplemental Material
- Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. In Proc. CASSIS, 2004.Google Scholar
- Bruno Barras and Bruno Bernardo. The Implicit Calculus of Constructions as a programming language with dependent types. In Proc. FoSSaCS, 2008. Google ScholarDigital Library
- Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Proc. FMCO, 2005. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- Bor-Yuh Evan Chang and Xavier Rival. Relational inductive shape analysis. In Proc. POPL, 2008. Google ScholarDigital Library
- Arthur Charguéraud and François Pottier. Functional translation of a calculus of capabilities. In Proc. ICFP, 2008. Google ScholarDigital Library
- Chiyan Chen and Hongwei Xi. Combining programming with theorem proving. In Proc. ICFP, 2005. Google ScholarDigital Library
- David Delahaye. A tactic language for the system Coq. In Proc. LPAR, 2000. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Bryan Ford. Parsing expression grammars: A recognition-based syntactic foundation. In Proc. POPL, 2004. Google ScholarDigital Library
- Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. Sage: Hybrid checking for flexible specifications. In Proc. Scheme Workshop, 2006.Google Scholar
- 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. Google ScholarDigital Library
- Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Proc. POPL, 2006. Google ScholarDigital Library
- Barbara Liskov and Stephen N. Zilles. Specification techniques for data abstractions. IEEE Trans. Software Eng., 1 (1): 7--19, 1975.Google ScholarDigital Library
- Conor McBride and James McKinna. The view from the left. J. Functional Programming, 14 (1): 69--111, 2004. Google ScholarDigital Library
- Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Polymorphism and separation in Hoare Type Theory. Proc. ICFP, 2006. Google ScholarDigital Library
- Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: Reasoning with the awkward squad. In Proc. ICFP, 2008.Google Scholar
- Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007.Google Scholar
- Emir Pasalic, Jeremy Siek, Walid Taha, and Seth Fogarty. Concoqtion: Indexed types now! In Proc. PEPM, 2007. Google ScholarDigital Library
- Lawrence C Paulson. Isabelle: A generic theorem prover. Journal of Automated Reasoning, 5, 1994.Google Scholar
- Rasmus L. Petersen, Lars Birkedal, Aleksandar Nanevski, and Greg Morrisett. A realizability model for impredicative Hoare Type Theory. In Proc. ESOP, 2008. Google ScholarDigital Library
- John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. LICS, 2002. Google ScholarDigital Library
- Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. ACM TOPLAS, 24, 2002. Google ScholarDigital Library
- Wouter Swierstra and Thorsten Altenkirch. Beauty in the beast: A functional semantics for the awkward squad. In Proc. Haskell Workshop, 2007. Google ScholarDigital Library
- Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In Proc. PLDI, 2008. Google ScholarDigital Library
Index Terms
- Effective interactive proofs for higher-order imperative programs
Recommendations
Effective interactive proofs for higher-order imperative programs
ICFP '09We 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, ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesWhen using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Interactive proofs in higher-order concurrent separation logic
POPL '17When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Comments