Verified heap theorem prover by paramodulation

Gordon Stewart, Lennart Beringer, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Scopus citations


We present VeriStar, a verified theorem prover for a decidable subset of separation logic. Together with VeriSmall [3], a proved-sound Smallfoot-style program analysis for C minor, VeriStar demonstrates that fully machine-checked static analyses equipped with efficient theorem provers are now within the reach of formal methods. As a pair, VeriStar and VeriSmall represent the first application of the Verified Software Toolchain [4], a tightly integrated collection of machine-verified program logics and compilers giving foundational correctness guarantees. VeriStar is (1) purely functional, (2) machine-checked, (3) end-to-end, (4) efficient and (5) modular. By purely functional, we mean it is implemented in Gallina, the pure functional programming language embedded in the Coq theorem prover. By machine-checked, we mean it has a proof in Coq that when the prover says "valid", the checked entailment holds in a proved-sound separation logic for C minor. By end-to-end, we mean that when the static analysis+theorem prover says a C minor program is safe, the program will be compiled to a semantically equivalent assembly program that runs on real hardware. By efficient, we mean that the prover implements a state-of-the-art algorithm for deciding heap entailments and uses highly tuned verified functional data structures. By modular, we mean that VeriStar can be retrofitted to other static analyses as a plug-compatible entailment checker and its soundness proof can easily be ported to other separation logics.

Original languageEnglish (US)
Title of host publicationICFP'12 - Proceedings of the 2012 ACM SIGPLAN International Conference on Functional Programming
Number of pages12
StatePublished - 2012
Event17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012 - Copenhagen, Denmark
Duration: Sep 9 2012Sep 15 2012

Publication series

NameProceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP


Other17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012

All Science Journal Classification (ASJC) codes

  • Software


  • paramodulation
  • separation logic
  • theorem proving


Dive into the research topics of 'Verified heap theorem prover by paramodulation'. Together they form a unique fingerprint.

Cite this