Back to the future: revisiting precise program verification using SMT solvers

ABSTRACT

This paper takes a fresh look at the problem of precise verification of heap-manipulating programs using first-order Satisfiability-Modulo-Theories (SMT) solvers. We augment the specification logic of such solvers by introducing the Logic of Interpreted Sets and Bounded Quantification for specifying properties of heap-manipulating programs. Our logic is expressive, closed under weakest preconditions, and efficiently implementable on top of existing SMT solvers. We have created a prototype implementation of our logic over the solvers Simplify and Z3 and used our prototype to verify many programs. Our preliminary experience is encouraging; the completeness and the efficiency of the decisionprocedure is clearly evident in practice and has greatly improved the user experience of the verifier.

REFERENCES

• 1: I. Balaban, A. Pnueli, and L.D. Zuck. Shape analysis by predicate abstraction. In Verification, Model checking, and Abstract Interpretation (VMCAI '05), LNCS 3385, pages 164--180, 2005.
• 2: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 3: Mike Barnett , K. Rustan M. Leino, Weakest-precondition of unstructured programs, Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, September 05-06, 2005, Lisbon, Portugal
• 4: M. Barnett, K.R.M. Leino, and W. Schulte. The Spec# programming system: An overview. In Construction and Analysis of Safe, Secure and Interoperable Smart Devices, LNCS 3362, pages 49--69, 2005.
• 5: J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O'Hearn, T. Wies, and H. Yang. Shape analysis for composite data structures. In Computer Aided Verification (CAV '07), LNCS 4590, pages 178--192, 2007.
• 6: J. Berdine, C. Calcagno, and P.W. O'Hearn. A decidable fragment of separation logic. In FSTTCS '04: Foundations of Software Technology and Theoretical Computer Science, LNCS 3328, pages 97--109, 2004.
• 7: E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer-Verlag, 1997.
• 8: S. Chatterjee, S.K. Lahiri, S. Qadeer, and Z. Rakamarić. A reachability predicate for analyzing low-level software. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS '07), LNCS 4424, pages 19--33, 2007.
• 9: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 10: L. de Moura and N. Bjorner. Efficient Incremental E-matching for SMT Solvers. In Conference on Automated Deduction (CADE '07), LNCS 4603, pages 183--198, 2007.
• 11: R. DeLine and K.R.M. Leino. BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research, 2005.
• 12: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 13: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 14: D. Distefano, P.W. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS '06), LNCS 3920, pages 287--302, 2006.
• 15: B. Dutertre and L.M. de Moura. A Fast Linear-Arithmetic Solver for DPLL(T). In Computer Aided Verification (CAV '06), LNCS 4144, pages 81--94, 2006.
• 16: 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
• 17: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 18: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 19: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 20: V. Kuncak and M.C. Rinard. Decision procedures for set-valued fields. Electr. Notes Theor. Comput. Sci., 131:51--62, 2005.
• 21: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 22: Shuvendu K. Lahiri , Shaz Qadeer, Verifying properties of well-founded linked lists, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.115-126, January 11-13, 2006, Charleston, South Carolina, USA
• 23: S.K. Lahiri and S. Qadeer. Back to the Future: Revisiting Precise Program Verification using SMT Solvers. Technical Report MSR-TR-2007-88, Microsoft Research, 2007.
• 24: S.K. Lahiri and S. Qadeer. A decision procedure for well-founded reachability. Technical Report MSR-TR-2007-43, Microsoft Research, 2007.
• 25: T. Lev-Ami, N. Immerman, T.W. Reps, S. Sagiv, S. Srivastava, and G. Yorsh. Simulating reachability using first-order logic with applications to verification of linked data structures. In Conference on Automated Deduction (CADE '05), LNCS 3632, pages 99--115, 2005.
• 26: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 27: S. McPeak and G.C. Necula. Data structure specifications via local equality axioms. In Computer-Aided Verification (CAV '05), LNCS 3576, pages 476--490, 2005.
• 28: Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.221-231, June 2001, Snowbird, Utah, United States
• 29: Muh. Available at http://muh.sourceforge.net/.
• 30: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 31: Greg Nelson, Verifying reachability invariants of linked structures, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.38-47, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567073]
• 32: Z. Rakamarić, J. Bingham, and A.J. Hu. An inference-rule-based decision procedure for verification of heap-manipulating programs with mutable data and cyclic data structures. In Verification, Model Checking, and Abstract Interpretation (VMCAI '06), LNCS 4349, pages 106--121, 2007.
• 33: Silvio Ranise , Calogero Zarba, A Theory of Singly-Linked Lists and its Extensible Decision Procedure, Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, p.206-215, September 11-15, 2006 [doi>10.1109/SEFM.2006.7]
• 34: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 35: Satisfiability Modulo Theories Library (SMT-LIB). Available at http://goedel.cs.uiowa.edu/smtlib/.
• 36: G. Yorsh, A.M. Rabinovich, M. Sagiv, A. Meyer, and A. Bouajjani. A logic of reachable patterns in linked data--structures. In Foundations of Software Science and Computation Structures (FoSSaCS '06), LNCS 3921, pages 94--110, 2006.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

General Terms:
Verification

Keywords:
SMT solvers, decision procedures, heap-manipulating programs, linked lists, reachability, software verification