An integrated proof language for imperative programs

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.

REFERENCES

• 1: 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.
• 2: Peter B. Andrews, Introduction to Mathematical Logic and Type Theory: To Truth through Proof, Kluwer Academic Publishers, Norwell, MA, 2002
• 3: Konstantinos Arkoudas , Olin Shivers, Denotational proof languages, Massachusetts Institute of Technology, 2000
• 4: K. Arkoudas, K. Zee, V. Kuncak, and M. Rinard. Verifying a file system implementation. In ICFEM, volume 3308 of LNCS, 2004.
• 5: David Aspinall, Proof General: A Generic Tool for Proof Development, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.38-42, March 25-April 02, 2000
• 6: R.-J. Back and J. von Wright. Refinement Calculus. Springer-Verlag, 1998.
• 7: I. Balaban, A. Pnueli, and L. Zuck. Shape analysis by predicate abstraction. In VMCAI'05, 2005.
• 8: Michael Balser , Wolfgang Reif , Gerhard Schellhorn , Kurt Stenzel , Andreas Thums, Formal System Development with KIV, Proceedings of the Third Internationsl Conference on Fundamental Approaches to Software Engineering: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.363-366, March 25-April 02, 2000
• 9: 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.
• 10: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 11: R. S. Boyer , J. S. Moore, Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic, Machine intelligence 11, Oxford University Press, Inc., New York, NY, 1988
• 12: P. Chalin, C. Hurlin, and J. Kiniry. Integrating static checking and interactive verification: Supporting multiple theories and provers in verification. In VSTTE, 2005.
• 13: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 14: A. Darvas and P. Muller. Formal encoding of JML Level 0 specifications in JIVE. Technical Report 559, Chair of Software Engineering, ETH Zurich, 2007.
• 15: Leonardo Moura , Nikolaj Bjørner, Efficient E-Matching for SMT Solvers, Proceedings of the 21st international conference on Automated Deduction: Automated Deduction, July 17-20, 2007, Bremen, Germany [doi>10.1007/978-3-540-73595-3_13]
• 16: D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Technical Report 159, COMPAQ Systems Research Center, 1998.
• 17: Jean-Christophe Filliâtre, Verification of non-functional programs using interpretations in type theory, Journal of Functional Programming, v.13 n.4, p.709-745, July 2003 [doi>10.1017/S095679680200446X]
• 18: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 19: Cormac Flanagan , Shaz Qadeer, Predicate abstraction for software verification, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-202, January 16-18, 2002, Portland, Oregon
• 20: Cormac Flanagan , James B. Saxe, Avoiding exponential explosion: generating compact verification conditions, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.193-205, January 2001, London, United Kingdom
• 21: J. Gallier. Logic for Computer Science. http://www.cis.upenn.edu/~jean/gbooks/logic.html, revised on-line edition, 2003.
• 22: Yeting Ge , Clark Barrett , Cesare Tinelli, Solving Quantified Verification Conditions Using Satisfiability Modulo Theories, Proceedings of the 21st international conference on Automated Deduction: Automated Deduction, July 17-20, 2007, Bremen, Germany [doi>10.1007/978-3-540-73595-3_12]
• 23: 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.
• 24: Viktor Kuncak , Martin C. Rinard, Modular data structure verification, Massachusetts Institute of Technology, Cambridge, MA, 2007
• 25: Viktor Kuncak , Patrick Lam , Karen Zee , Martin C. Rinard, Modular Pluggable Analyses for Data Structure Consistency, IEEE Transactions on Software Engineering, v.32 n.12, p.988-1005, December 2006 [doi>10.1109/TSE.2006.125]
• 26: 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.
• 27: Viktor Kuncak , Huu Hai Nguyen , Martin Rinard, Deciding Boolean Algebra with Presburger Arithmetic, Journal of Automated Reasoning, v.36 n.3, p.213-239, April 2006 [doi>10.1007/s10817-006-9042-1]
• 28: V. Kuncak and M. Rinard. Existential heap abstraction entailment is undecidable. In Static Analysis Symposium, 2003.
• 29: Viktor Kuncak , Martin Rinard, Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic, Proceedings of the 21st international conference on Automated Deduction: Automated Deduction, July 17-20, 2007, Bremen, Germany [doi>10.1007/978-3-540-73595-3_15]
• 30: Patrick Lam , Martin Rinard, The hob system for verifying software design properties, Massachusetts Institute of Technology, Cambridge, MA, 2007
• 31: Patrick Lam , Viktor Kuncak , Martin Rinard, Crosscutting techniques in program specification and analysis, Proceedings of the 4th international conference on Aspect-oriented software development, p.169-180, March 14-18, 2005, Chicago, Illinois [doi>10.1145/1052898.1052913]
• 32: K. R. M. Leino. This is Boogie 2. http://research.microsoft.com/leino/papers/krml178.pdf, June 2008. (working draft).
• 33: J. Meng and L. C. Paulson. Translating higher-order problems to first-order clauses. In ESCoR: Empir. Successful Comp. Reasoning, pages 70--80, 2006.
• 34: Aleksandar Nanevski , Greg Morrisett , Avraham Shinnar , Paul Govereau , Lars Birkedal, Ynot: dependent types for imperative programs, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, September 20-28, 2008, Victoria, BC, Canada
• 35: Isabelle/HOL: a proof assistant for higher-order logic, Springer-Verlag, London, 2002
• 37: Bengt Nordström , Kent Petersson , Jan M. Smith, Programming in Martin-Lo¨f's type theory: an introduction, Clarendon Press, New York, NY, 1990
• 38: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 39: Lawrence C. Paulson, Logic and computation: interactive proof with Cambridge LCF, Cambridge University Press, New York, NY, 1987
• 40: 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.
• 41: Piotr Rudnicki , Andrzej Trybulec, On Equivalents of Well-Foundedness, Journal of Automated Reasoning, v.23 n.3, p.197-234, November 1999 [doi>10.1023/A:1006218513245]
• 42: Stephan Schulz, E - a brainiac theorem prover, AI Communications, v.15 n.2,3, p.111-126, August 2002
• 43: 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.
• 44: Christoph Weidenbach, Combining superposition, sorts and splitting, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 45: M. Wenzel. Isabelle/Isar -- a versatile environment for human-readable formal proof documents. PhD thesis, TU Munchen, 2002.
• 46: Hongwei Xi, Dependent ML An approach to practical programming with dependent types, Journal of Functional Programming, v.17 n.2, p.215-286, March 2007 [doi>10.1017/S0956796806006216]
• 47: Karen Zee , Viktor Kuncak , Martin Rinard, Full functional verification of linked data structures, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Algorithms, Languages, Reliability, Verification

Keywords:
proof system, theorem prover, verification