Program verification using templates over predicate abstraction

ABSTRACT

We address the problem of automatically generating invariants with quantified and boolean structure for proving the validity of given assertions or generating pre-conditions under which the assertions are valid. We present three novel algorithms, having different strengths, that combine template and predicate abstraction based formalisms to discover required sophisticated program invariants using SMT solvers.

Two of these algorithms use an iterative approach to compute fixed-points (one computes a least fixed-point and the other computes a greatest fixed-point), while the third algorithm uses a constraint based approach to encode the fixed-point. The key idea in all these algorithms is to reduce the problem of invariant discovery to that of finding optimal solutions for unknowns (over conjunctions of some predicates from a given set) in a template formula such that the formula is valid.

Preliminary experiments using our implementation of these algorithms show encouraging results over a benchmark of small but complicated programs. Our algorithms can verify program properties that, to our knowledge, have not been automatically verified before. In particular, our algorithms can generate full correctness proofs for sorting algorithms (which requires nested universally-existentially quantified invariants) and can also generate preconditions required to establish worst-case upper bounds of sorting algorithms. Furthermore, for the case of previously considered properties, in particular sortedness in sorting algorithms, our algorithms take less time than reported by previous techniques.

REFERENCES

• 1: Dirk Beyer, Thomas Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Invariant synthesis for combined theories. In VMCAI, volume 4349 of LNCS, pages 378--394, 2007.
• 2: Dirk Beyer , Thomas A. Henzinger , Rupak Majumdar , Andrey Rybalchenko, Path invariants, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 3: 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
• 4: Michael Colon, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. In CAV, pages 420--432, 2003.
• 5: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 6: 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]
• 7: Leonardo de Moura and Nikolaj Bjorner. Z3: Efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337--340, April 2008.
• 8: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 9: 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
• 10: 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
• 11: Sumit Gulwani , Sagar Jain , Eric Koskinen, Control-flow refinement and progress invariants for bound analysis, Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation, June 15-21, 2009, Dublin, Ireland
• 12: Sumit Gulwani , Bill McCloskey , Ashish Tiwari, Lifting abstract interpreters to quantified logical domains, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 13: Sumit Gulwani , Saurabh Srivastava , Ramarathnam Venkatesan, Program analysis as constraint solving, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 14: Sumit Gulwani , Saurabh Srivastava , Ramarathnam Venkatesan, Constraint-Based Invariant Inference over Predicate Abstraction, Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation, December 18-20, 2008, Savannah, GA [doi>10.1007/978-3-540-93900-9_13]
• 15: Nicolas Halbwachs , Mathias Péron, Discovering properties about arrays in simple programs, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 16: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-244, January 14-16, 2004, Venice, Italy
• 17: Ranjit Jhala and Ken McMillan. Array abstraction from proofs. In CAV, 2007.
• 18: Deepak Kapur. Automatically generating loop invariants using quantifier elimination. In Deduction and Applications, 2005.
• 19: Gary A. Kildall, A unified approach to global program optimization, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-206, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512945]
• 20: Laura Kovács , Andrei Voronkov, Finding Loop Invariants for Programs over Arrays Using a Theorem Prover, Proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, March 22-29, 2009, York, UK [doi>10.1007/978-3-642-00593-0_33]
• 21: Shuvendu K. Lahiri , Randal E. Bryant, Predicate abstraction with indexed predicates, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.4-es, December 2007 [doi>10.1145/1297658.1297662]
• 22: Andreas Podelski and Thomas Wies. Boolean heaps. In SAS, 2005.
• 23: Thomas W. Reps, Shmuel Sagiv, and Greta Yorsh. Symbolic impl. of the best transformer. In VMCAI, pages 252--266, 2004.
• 24: Microsoft Research. Phoenix. http://research.microsoft.com/Phoenix/.
• 25: Microsoft Research. Z3. http://research.microsoft.com/projects/Z3/.
• 26: Sriram Sankaranarayanan , Henny B. Sipma , Zohar Manna, Non-linear loop invariant generation using Gröbner bases, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.318-329, January 14-16, 2004, Venice, Italy
• 27: Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. Constraint-based linear-relations analysis. In SAS, pages 53--68, 2004.
• 28: Armando Solar-Lezama , Gilad Arnold , Liviu Tancau , Rastislav Bodik , Vijay Saraswat , Sanjit Seshia, Sketching stencils, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 29: Armando Solar-Lezama , Liviu Tancau , Rastislav Bodik , Sanjit Seshia , Vijay Saraswat, Combinatorial sketching for finite programs, Proceedings of the 12th international conference on Architectural support for programming languages and operating systems, October 21-25, 2006, San Jose, California, USA
• 30: Saurabh Srivastava and Sumit Gulwani. Program verification using templates over predicate abstraction. Technical Report MSR-TR-2008-173, Nov 2008.
• 31: Saurabh Srivastava, Sumit Gulwani, and Jeffrey Foster. VS3 : SMT-solvers for program verification. In CAV, 2009.
• 32: 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:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Correctness proofs

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification; Logics of programs; Pre- and post-conditions
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
constraint-based fixed-point, iterative fixed-point, predicate abstraction, quantified invariants, smt solvers, template invariants, weakest preconditions