Gordon Stewart
Andrew W. Appel
ABSTRACT
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.
- URL http://www.cs.princeton.edu/~jsseven/p/veristar.Google Scholar
- A. W. Appel. Foundational proof-carrying code. In LICS, 2001. Google ScholarDigital Library
- A. W. Appel. VeriSmall: Verified Smallfoot shape analysis. In First International Conf. on Certified Programs and Proofs, Dec. 2011. Google ScholarDigital Library
- A. W. Appel. Verified Software Toolchain. In ESOP, pages 1--17, 2011. Google ScholarDigital Library
- M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry, and B. Werner. A modular integration of SAT/SMT solvers to Coq through proof witnesses. In First International Conf. on Certified Programs and Proofs, 2011. Google ScholarDigital Library
- R. Atkey. Amortised resource analysis with separation logic. Logical Methods in Computer Science, 7 (2:17), 2011.Google ScholarCross Ref
- L. Bachmair and H. Ganzinger. Equational Reasoning in Saturation-Based Theorem Proving. In W. Bibel and P. Schmitt, editors, Automated Deduction - A Basis for Applications, volume I, 1998. Google ScholarDigital Library
- J. L. Bentley. Writing Efficient Programs. Prentice-Hall, 1982. Google ScholarDigital Library
- J. Berdine, C. Calcagno, and P. W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Formal Methods for Components and Objects, pages 115--135, 2005. Google ScholarDigital Library
- J. Berdine, B. Cook, and S. Ishtiaq. SLAyer: Memory safety for systems-level code. In CAV, pages 178--183, 2011. Google ScholarDigital Library
- F. Besson, P.-E. Cornilleau, and D. Pichardie. Modular SMT proofs for fast reflexive checking inside Coq. In First International Conf. on Certified Programs and Proofs, 2011. Google ScholarDigital Library
- T. Braibant and D. Pous. Tactics for reasoning modulo AC in Coq. In First International Conf. on Certified Programs and Proofs, 2011. Google ScholarDigital Library
- J. Brotherston, D. Distefano, and R. L. Petersen. Automated cyclic entailment proofs in separation logic. In Proceedings of CADE-23, pages 131--146, 2011. Google ScholarDigital Library
- C. Calcagno and D. Distefano. Infer: an automatic program verifier for memory safety of C programs. In Third International Conference on NASA Formal Methods, pages 459--465, 2011. Google ScholarDigital Library
- C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction. SIGPLAN Not., 44: 289--300, January 2009. Google ScholarDigital Library
- B.-Y. E. Chang and X. Rival. Relational inductive shape analysis. In POPL, pages 247--260, 2008. Google ScholarDigital Library
- A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI'11, pages 234--245, 2011. Google ScholarDigital Library
- L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008. Google ScholarDigital Library
- D. Distefano and M. J. Parkinson J. jStar: Towards practical verification for Java. In OOPSLA, 2008. Google ScholarDigital Library
- R. Dockins, A. Hobor, and A. W. Appel. A fresh look at separation algebras and share accounting. In APLAS: 7th Asian Symposium on Programming Languages and Systems, pages 161--177, 2009. Google ScholarDigital Library
- S. L. Graham, P. B. Kessler, and M. K. McKusick. Gprof: A call graph execution profiler. In Proc. SIGPLAN '82 Symp. on Compiler Construction, SIGPLAN Notices, pages 120--126. ACM Press, 1982. Google ScholarDigital Library
- A. Hobor, A. W. Appel, and F. Zappa Nardelli. Oracle Semantics for Concurrent Separation Logic. In ESOP, pages 353--367, 2008. Google ScholarDigital Library
- X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43 (4): 363--446, 2009. Google ScholarDigital Library
- B. Löchner and S. Schulz. An evaluation of shared rewriting. In Proceedings of the Second International Workshop on Implementation of Logics, Technical Report MPI-I-2001-2-006, pages 33--48, 2001.Google Scholar
- S. Magill, A. Nanevski, E. Clarke, and P. Lee. Inferring invariants in separation logic for imperative list-processing programs. In Third Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE), 2006.Google Scholar
- J. A. Navarro Pérez and A. Rybalchenko. Separation logic + superposition calculus = heap theorem prover. In PLDI, pages 556--566, 2011. Google ScholarDigital Library
- G. Necula. Proof-carrying code. In POPL, pages 106--119, 1997. Google ScholarDigital Library
- G. C. Necula and P. Lee. Efficient representation and validation of proofs. In LICS, pages 93--104, 1998. Google ScholarDigital Library
- G. C. Necula and S. P. Rahul. Oracle-based checking of untrusted software. In POPL, pages 142--154, 2001. Google ScholarDigital Library
- H. H. Nguyen and W.-N. Chin. Enhancing program verification with lemmas. In CAV, pages 355--369, 2008. Google ScholarDigital Library
- H. H. Nguyen, C. David, S. Qin, and W.-N. Chin. Automated verification of shape and size properties via separation logic. In VMCAI, pages 251--266, 2007. Google ScholarDigital Library
- R. Nieuwenhuis and A. Rubio. Paramodulation-based theorem proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, 2001.Google ScholarCross Ref
- T. Tuerk. A formalisation of Smallfoot in HOL. In Theorem Proving in Higher Order Logics, pages 469--484, 2009. Google ScholarDigital Library
Index Terms
- Verified heap theorem prover by paramodulation
Recommendations
Verified heap theorem prover by paramodulation
ICFP '12We 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 ...
Separation logic + superposition calculus = heap theorem prover
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and ImplementationProgram analysis and verification tools crucially depend on the ability to symbolically describe and reason about sets of program behaviors. Separation logic provides a promising foundation for dealing with heap manipulating programs, while the ...
DT-an automated theorem prover for multiple-valued first-order predicate logics
ISMVL '96: Proceedings of the 26th International Symposium on Multiple-Valued LogicWe describe the automated theorem prover "Deep Thought" (DT). The prover can be used for arbitrary multiple-valued first-order logics, provided the connectives can be defined by truth tables and the quantifiers are generalizations of the classical ...
Comments