TY - JOUR

T1 - Verified heap theorem prover by paramodulation

AU - Stewart, Gordon

AU - Beringer, Lennart

AU - Appel, Andrew W.

PY - 2012/9/1

Y1 - 2012/9/1

N2 - 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.

AB - 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.

KW - Paramodulation

KW - Separation Logic

KW - Theorem Proving

UR - http://www.scopus.com/inward/record.url?scp=84870451001&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84870451001&partnerID=8YFLogxK

U2 - 10.1145/2398856.2364531

DO - 10.1145/2398856.2364531

M3 - Article

AN - SCOPUS:84870451001

VL - 47

SP - 3

EP - 14

JO - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

JF - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

SN - 1523-2867

IS - 9

ER -