Program analysis as constraint solving

ABSTRACT

A constraint-based approach to invariant generation in programs translates a program into constraints that are solved using off-the-shelf constraint solvers to yield desired program invariants.

In this paper we show how the constraint-based approach can be used to model a wide spectrum of program analyses in an expressive domain containing disjunctions and conjunctions of linear inequalities. In particular, we show how to model the problem of context-sensitive interprocedural program verification. We also present the first constraint-based approach to weakest precondition and strongest postcondition inference. The constraints we generate are boolean combinations of quadratic inequalities over integer variables. We reduce these constraints to SAT formulae using bitvector modeling and use off-the-shelf SAT solvers to solve them.

Furthermore, we present interesting applications of the above analyses, namely bounds analysis and generation of most-general counter-examples for both safety and termination properties. We also present encouraging preliminary experimental results demonstrating the feasibility of our technique on a variety of challenging examples.

REFERENCES

• 1: I. Balaban, A. Cohen, and A. Pnueli. Ranking abstraction of recursive programs. In VMCAI, pages 267--281, 2006.
• 2: Josh Berdine , Aziem Chawdhary , Byron Cook , Dino Distefano , Peter O'Hearn, Variance analyses from invariance analyses, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 3: D. Beyer, T. Henzinger, R. Majumdar, and A. Rybalchenko. Invariant synthesis for combined theories. In VMCAI07, pages 378--394, 2007.
• 4: 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
• 5: Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérôme Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
• 6: A. R. Bradley and Z. Manna. Verification constraint problems with strengthening. In ICTAC, pages 35--49, 2006.
• 7: A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with reachability. In Proc. 17th Intl. Conference on Computer Aided Verification (CAV), volume 3576 of Lecture Notes in Computer Science. Springer Verlag, July 2005.
• 8: M. Colon, S. Sankaranarayanan, and H. Sipma. Linear invariant generation using non-linear constraint solving. In CAV, pages 420--432, 2003.
• 9: Michael Colón , Henny Sipma, Practical Methods for Proving Program Termination, Proceedings of the 14th International Conference on Computer Aided Verification, p.442-454, July 27-31, 2002
• 10: P. Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In VMCAI, pages 1--24, 2005.
• 11: 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]
• 12: L. M. de Moura and N. Bjrner. Efficient e-matching for smt solvers. In CADE, pages 183--198, 2007.
• 13: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 14: Roberto Giacobazzi , Francesco Ranzato, Optimal domains for disjunctive abstract interpretation, Science of Computer Programming, v.32 n.1-3, p.177-210, Sept. 1998 [doi>10.1016/S0167-6423(97)00034-8]
• 15: L. Gonnord and N. Halbwachs. Combining widening and acceleration in linear relation analysis. In 13th International Static Analysis Symposium, SAS06, LNCS 4134, Aug. 2006.
• 16: D. Gopan and T. W. Reps. Lookahead widening. In CAV, pages 452--466, 2006.
• 17: D. Gopan and T. W. Reps. Guided static analysis. In SAS, pages 349--365, 2007.
• 18: B. S. Gulavani, S. Chakraborty, A. V. Nori, and S. K. Rajamani. Automatically refining abstract interpretations. Technical Report TR-07-23, IIT Bombay, 2007.
• 19: B. S. Gulavani and S. K. Rajamani. Counterexample driven refinement for abstract interpretation. In TACAS, pages 474--488, 2006.
• 20: S. Gulwani, K. Mehra, and T. Chilimbi. Statically computing complexity bounds for programs with recursive data-structures. Technical Report MSR-TR-2008-16, Microsoft Research, Jan. 2008.
• 21: S. Gulwani, S. Srivastava, and R. Venkatesan. Program analysis as constraint solving. Full version. Technical Report MSR-TR-2008-44, Microsoft Research, Mar. 2008.
• 22: Ashutosh Gupta , Thomas A. Henzinger , Rupak Majumdar , Andrey Rybalchenko , Ru-Gang Xu, Proving non-termination, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 23: C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321--332, 1983.
• 24: D. Kapur. Automatically generating loop invariants using quantifier elimination. In Deduction and Applications, 2005.
• 25: 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]
• 26: Z. Manna. Mathematical Theory of Computation. McGraw-Hill, New York, 74.
• 27: Z. Manna and J. McCarthy. Properties of programs and partial function logic. Machine Intelligence, 5, 1970.
• 28: Zohar Manna , Amir Pnueli, Formalization of Properties of Functional Programs, Journal of the ACM (JACM), v.17 n.3, p.555-569, July 1970 [doi>10.1145/321592.321606]
• 29: Markus Müller-Olm , Helmut Seidl, Precise interprocedural analysis through linear algebra, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.330-341, January 14-16, 2004, Venice, Italy
• 30: M. Muller-Olm, H. Seidl, and B. Steffen. Interprocedural analysis (almost) for free. In Technical Report 790, Fachbereich Informatik, Universitt Dortmund, 2004.
• 31: M. Muller-Olm, H. Seidl, and B. Steffen. Interprocedural herbrand equalities. In ESOP, pages 31--45, 2005.
• 32: A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI, pages 239--251, 2004.
• 33: Mooly Sagiv , Thomas Reps , Susan Horwitz, Precise interprocedural dataflow analysis with applications to constant propagation, Theoretical Computer Science, v.167 n.1-2, p.131-170, Oct. 30, 1996
• 34: S. Sankaranarayanan, F. Ivancic, I. Shlyakhter, and A. Gupta. Static analysis in disjunctive numerical domains. In SAS, pages 317, 2006. {35} S. Sankaranarayanan, H. Sipma, and Z. Manna. Non-linear loop invariant generation using grobner bases. In POPL, pages 318--329, 2004.
• 35: S. Sankaranarayanan, H. B. Sipma, and Z. Manna. Constraint-based linear-relations analysis. In SAS, pages 53--68, 2004.
• 36: S. Sankaranarayanan, H. B. Sipma, and Z. Manna. Scalable analysis of linear systems using mathematical programming. In VMCAI, pages 25--41, 2005.
• 37: Alexander Schrijver, Theory of linear and integer programming, John Wiley & Sons, Inc., New York, NY, 1986
• 38: H. Seidl, A. Flexeder, and M. Petter. Interprocedurally analysing linear inequality relations. In ESOP, pages 284--299, 2007.
• 39: C. Wang, Z. Yang, A. Gupta, and F. Ivancic. Using counterex. for improv. the prec. of reachability comput. with polyhedra. In CAV, pages 352--365, 2007.
• 40: Y. Xie and A. Aiken. Saturn: A sat-based tool for bug detection. In CAV, pages 139--143, 2005.

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, Theory, Verification

Keywords:
bounds analysis, constraint solving, most-general counterexamples, non-termination analysis, program verification, strongest postcondition, weakest precondition