Effective Interactive Proofs for Higher-Order Imperative Programs

DSpace/Manakin Repository

Effective Interactive Proofs for Higher-Order Imperative Programs

Citable link to this page


Title: Effective Interactive Proofs for Higher-Order Imperative Programs
Author: Chlipala, Adam J.; Malecha, Gregory Michael; Morrisett, John Gregory; Shinnar, Avraham Ever; Wisnesky, Ryan

Note: Order does not necessarily reflect citation order of authors.

Citation: Chlipala, Adam J., Gregory Michael Malecha, John Gregory Morrisett, Avraham Ever Shinnar, and Ryan Wisnesky. 2009. Effective interactive proofs for higher-order imperative programs. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming : August 31-September 2, 2009, Edinburgh, Scotland, ed. G. Grutton, 79-90. New York: ACM Press.
Full Text & Related Files:
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.
Published Version: http://portal.acm.org/citation.cfm?id=1596550.1596565&coll=GUIDE&dl=GUIDE&type=series&idx=SERIES824&part=series&WantType=Proceedings&title=ICFP&CFID=83733044&CFTOKEN=93852205
Other Sources: http://ynot.cs.harvard.edu/papers/icfp09.pdf
Terms of Use: This article is made available under the terms and conditions applicable to Open Access Policy Articles, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#OAP
Citable link to this page: http://nrs.harvard.edu/urn-3:HUL.InstRepos:4686803
Downloads of this work:

Show full Dublin Core record

This item appears in the following Collection(s)


Search DASH

Advanced Search