Karen Zee
Viktor Kuncak
ABSTRACT
We present an integrated proof language for guiding the actions of multiple reasoning systems as they work together to prove complex correctness properties of imperative programs. The language operates in the context of a program verification system that uses multiple reasoning systems to discharge generated proof obligations. It is designed to 1) enable developers to resolve key choice points in complex program correctness proofs, thereby enabling automated reasoning systems to successfully prove the desired correctness properties; 2) allow developers to identify key lemmas for the reasoning systems to prove, thereby guiding the reasoning systems to find an effective proof decomposition; 3) enable multiple reasoning systems to work together productively to prove a single correctness property by providing a mechanism that developers can use to divide the property into lemmas, each of which is suitable for a different reasoning system; and 4) enable developers to identify specific lemmas that the reasoning systems should use when attempting to prove other lemmas or correctness properties, thereby appropriately confining the search space so that the reasoning systems can find a proof in an acceptable amount of time.
The language includes a rich set of declarative proof constructs that enables developers to direct the reasoning systems as little or as much as they desire. Because the declarative proof statements are embedded into the program as specialized comments, they also serve as verified documentation and are a natural extension of the assertion mechanism found in most program verification systems.
We have implemented our integrated proof language in the context of a program verification system for Java and used the resulting system to verify a collection of linked data structure implementations. Our experience indicates that our proof language makes it possible to successfully prove complex program correctness properties that are otherwise beyond the reach of automated reasoning systems.
- W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hahnle, W. Menzel, W. Mostowski, A. Roth, S. Schlager, and P. H. Schmitt. The KeY tool. Software and System Modeling, 4:32--54, 2005.Google Scholar
Digital Library
- P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Springer (Kluwer), 2nd edition, 2002. Google ScholarDigital Library
- K. Arkoudas. Denotational Proof Languages. PhD thesis, Massachusetts Institute of Technology, 2000. Google ScholarDigital Library
- K. Arkoudas, K. Zee, V. Kuncak, and M. Rinard. Verifying a file system implementation. In ICFEM, volume 3308 of LNCS, 2004.Google Scholar
- D. Aspinall. Proof general: A generic tool for proof development. In TACAS, 2000. Google ScholarDigital Library
- R.-J. Back and J. von Wright. Refinement Calculus. Springer-Verlag, 1998.Google Scholar
- I. Balaban, A. Pnueli, and L. Zuck. Shape analysis by predicate abstraction. In VMCAI'05, 2005. Google ScholarDigital Library
- M. Balser, W. Reif, G. Schellhorn, K. Stenzel, and A. Thums. Formal system development with KIV. In FASE, number 1783 in LNCS, 2000. Google ScholarDigital Library
- M. Barnett, R. DeLine, M. Fahndrich, K. R. M. Leino, and W. Schulte. Verification of object-oriented programs with invariants. Journal of Object Technology, 3(6):27--56, 2004.Google ScholarCross Ref
- Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development-Coq'Art: The Calculus of Inductive Constructions. Springer, 2004. Google ScholarDigital Library
- R. S. Boyer and J. S. Moore. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In Machine Intelligence, volume 11, pages 83--124. OUP, 1988. Google ScholarDigital Library
- P. Chalin, C. Hurlin, and J. Kiniry. Integrating static checking and interactive verification: Supporting multiple theories and provers in verification. In VSTTE, 2005.Google Scholar
- T. Coquand and G. P. Huet. The calculus of constructions. Inf. Comput., 76(2/3):95--120, 1988. Google ScholarDigital Library
- A. Darvas and P. Muller. Formal encoding of JML Level 0 specifications in JIVE. Technical Report 559, Chair of Software Engineering, ETH Zurich, 2007.Google Scholar
- L. de Moura and N. Bjørner. Efficient E-matching for SMT solvers. In CADE, 2007. Google ScholarDigital Library
- D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Technical Report 159, COMPAQ Systems Research Center, 1998.Google Scholar
- J.-C. Filliatre. Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming, 13(4):709--745, 2003. Google ScholarDigital Library
- C. Flanagan, K. R. M. Leino, M. Lilibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended Static Checking for Java. In Proc. ACM PLDI, 2002. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In Proc. 29th ACM POPL, 2002. Google ScholarDigital Library
- C. Flanagan and J. B. Saxe. Avoiding exponential explosion: Generating compact verification conditions. In Proc. 28th ACM POPL, 2001. Google ScholarDigital Library
- J. Gallier. Logic for Computer Science. http://www.cis.upenn.edu/~jean/gbooks/logic.html, revised on-line edition, 2003.Google Scholar
- Y. Ge, C. Barrett, and C. Tinelli. Solving quantified verification conditions using satisfiability modulo theories. In CADE, 2007. Google ScholarDigital Library
- N. Immerman, A. M. Rabinovich, T.W. Reps, S. Sagiv, and G. Yorsh. The boundary between decidability and undecidability for transitive-closure logics. In Computer Science Logic, pages 160--174, 2004.Google ScholarCross Ref
- V. Kuncak. Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology, February 2007. Google ScholarDigital Library
- V. Kuncak, P. Lam, K. Zee, and M. Rinard. Modular pluggable analyses for data structure consistency. IEEE Transactions on Software Engineering, 32(12), December 2006. Google ScholarDigital Library
- V. Kuncak and K. R. M. Leino. In-place refinement for effect checking. In Second International Workshop on Automated Verification of Infinite-State Systems (AVIS'03), Warsaw, Poland, April 2003.Google Scholar
- V. Kuncak, H. H. Nguyen, and M. Rinard. Deciding Boolean Algebra with Presburger Arithmetic. J. of Automated Reasoning, 2006. http://dx.doi.org/10.1007/s10817--006--9042--1. Google ScholarDigital Library
- V. Kuncak and M. Rinard. Existential heap abstraction entailment is undecidable. In Static Analysis Symposium, 2003. Google ScholarDigital Library
- V. Kuncak and M. Rinard. Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In CADE-21, 2007. Google ScholarDigital Library
- P. Lam. The Hob System for Verifying Software Design Properties. PhD thesis, Massachusetts Institute of Technology, February 2007. Google ScholarDigital Library
- P. Lam, V. Kuncak, and M. Rinard. Cross-cutting techniques in program specification and analysis. In 4th International Conference on Aspect-Oriented Software Development (AOSD'05), 2005. Google ScholarDigital Library
- K. R. M. Leino. This is Boogie 2. http://research.microsoft.com/leino/papers/krml178.pdf, June 2008. (working draft).Google Scholar
- J. Meng and L. C. Paulson. Translating higher-order problems to first-order clauses. In ESCoR: Empir. Successful Comp. Reasoning, pages 70--80, 2006.Google Scholar
- A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: dependent types for imperative programs. In ICFP, pages 229--240, 2008. Google ScholarDigital Library
- T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer-Verlag, 2002. Google ScholarDigital Library
- B. Nordstroem, K. Petersson, and J. Smith. Programming in Martin-Loef's Type Theory: An Introduction. Oxford University Press, 1990. Google ScholarDigital Library
- S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In 11th CADE, 1992. Google ScholarDigital Library
- L. C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. CUP, 1987. Google ScholarDigital Library
- S. Ranise and C. Tinelli. The SMT-LIB Standard: Version 1.2. Technical report, Department of Computer Science, The University of Iowa, 2006. Available at www.SMT-LIB.org.Google Scholar
- P. Rudnicki and A. Trybulec. On equivalents of well-foundedness. J. Autom. Reasoning, 23(3-4):197--234, 1999. Google ScholarDigital Library
- S. Schulz. E -- A Brainiac Theorem Prover. Journal of AI Communications, 15(2/3):111--126, 2002. Google ScholarDigital Library
- J. van der Berg and B. Jacobs. The LOOP compiler for Java and UML. Technical Report CSI-R0019, Computing Science Institute, Univ. of Nijmegen, Dec. 2000.Google Scholar
- C. Weidenbach. Combining superposition, sorts and splitting. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 27. Elsevier Science, 2001. Google ScholarDigital Library
- M. Wenzel. Isabelle/Isar -- a versatile environment for human-readable formal proof documents. PhD thesis, TU Munchen, 2002.Google Scholar
- H. Xi. Dependent ML: An approach to practical programming with dependent types. J. Funct. Program., 17(2):215--286, 2007. Google ScholarDigital Library
- K. Zee, V. Kuncak, and M. Rinard. Full functional verification of linked data structures. In Proc. ACM PLDI, June 2008. Google ScholarDigital Library
Index Terms
- An integrated proof language for imperative programs
Recommendations
An integrated proof language for imperative programs
PLDI '09We present an integrated proof language for guiding the actions of multiple reasoning systems as they work together to prove complex correctness properties of imperative programs. The language operates in the context of a program verification system ...
A proof system for separation logic with magic wand
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesSeparation logic is an extension of Hoare logic which is acknowledged as an enabling technology for large-scale program verification. It features two new logical connectives, separating conjunction and separating implication, but most of the ...
A proof system for separation logic with magic wand
POPL '14Separation logic is an extension of Hoare logic which is acknowledged as an enabling technology for large-scale program verification. It features two new logical connectives, separating conjunction and separating implication, but most of the ...
Comments