Non-linear loop invariant generation using Gröbner bases

ABSTRACT

We present a new technique for the generation of non-linear (algebraic) invariants of a program. Our technique uses the theory of ideals over polynomial rings to reduce the non-linear invariant generation problem to a numerical constraint solving problem. So far, the literature on invariant generation has been focussed on the construction of linear invariants for linear programs. Consequently, there has been little progress toward non-linear invariant generation. In this paper, we demonstrate a technique that encodes the conditions for a given template assertion being an invariant into a set of constraints, such that all the solutions to these constraints correspond to non-linear (algebraic) loop invariants of the program. We discuss some trade-offs between the completeness of the technique and the tractability of the constraint-solving problem generated. The application of the technique is demonstrated on a few examples.

REFERENCES

• 1: Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1998
• 2: Ballarin, C., and Kauers, M. Solving parametric linear systems: an experiment with constraint algebraic programming. In Eighth Rhine Workshop on Computer Algebra (2002), pp. 101--114.
• 3: Saddek Bensalem , Marius Bozga , Jean-Claude Fernandez , Lucian Ghirvu , Yassine Lakhnech, A Transformational Approach for Generating Non-linear Invariants, Proceedings of the 7th International Symposium on Static Analysis, p.58-74, June 29-July 01, 2000
• 4: Saddek Bensalem , Yassine Lakhnech , Hassen Saïdi, Powerful Techniques for the Automatic Generation of Invariants, Proceedings of the 8th International Conference on Computer Aided Verification, p.323-335, August 03, 1996
• 5: Nikolaj Bjørner , Anca Browne , Zohar Manna, Automatic generation of invariants and intermediate assertions, Theoretical Computer Science, v.173 n.1, p.49-87, Feb. 1997 [doi>10.1016/S0304-3975(96)00191-0]
• 6: Tevfik Bultan , Richard Gerber , William Pugh, Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic, Proceedings of the 9th International Conference on Computer Aided Verification, p.400-411, June 22-25, 1997
• 7: George E. Collins, Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, p.134-183, May 20-23, 1975
• 8: George E. Collins , Hoon Hong, Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation, v.12 n.3, p.299-328, Sept. 1991 [doi>10.1016/S0747-7171(08)80152-6]
• 9: Colòn, M., Sankaranarayanan, S., and Sipma, H. Linear invariant generation using non-linear constraint solving. In Computer Aided Verification (July 2003), F. Somenzi and W. H. Jr, Eds., vol. 2725 of LNCS, Springer Verlag, pp. 420--433.
• 10: 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]
• 11: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 12: Cox, D., little, J., and O'Shea, D. Ideals, Varieties and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer, 1991.
• 13: Andreas Dolzmann , Thomas Sturn, REDLOG: computer algebra meets computer logic, ACM SIGSAM Bulletin, v.31 n.2, p.2-9, June 1997 [doi>10.1145/261320.261324]
• 14: Floyd, R. W. Assigning meanings to programs. Proc. Symposia in Applied Mathematics 19 (1967), 19--32.
• 15: Thomas A. Henzinger , Pei-Hsin Ho, HYTECH: The Cornell HYbrid TECHnology Tool, Hybrid Systems II, p.265-293, January 1995
• 16: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 17: J. Jaffar , J.-L. Lassez, Constraint logic programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.111-119, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41635]
• 18: Karr, M. Affine relationships among variables of a program. Acta Inf. 6 (1976), 133--151.
• 19: Zohar Manna, Introduction to Mathematical Theory of Computation, McGraw-Hill, Inc., New York, NY, 1974
• 20: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 21: Bud Mishra , Chee Yap, Notes on Grobner bases, Information Sciences: an International Journal, v.48 n.3, p.219-252, Aug. 1989 [doi>10.1016/0020-0255(89)90037-6]
• 22: Markus Müller-Olm , Helmut Seidl, Polynomial Constants Are Decidable, Proceedings of the 9th International Symposium on Static Analysis, p.4-19, September 17-20, 2002
• 23: Alexandeer Schrijver, Theory of linear and integer programming, John Wiley & Sons, Inc., New York, NY, 1986
• 24: William Y. Sit, An algorithm for solving parametric linear systems, Journal of Symbolic Computation, v.13 n.4, p.353-394, April 1992 [doi>10.1016/S0747-7171(08)80104-6]
• 25: Tarski, A. A decision method for elementary algebra and geometry. Univ. of California Press, Berkeley 5 (1951).
• 26: Ashish Tiwari , Harald Rueß , Hassen Saïdi , Natarajan Shankar, A Technique for Invariant Generation, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.113-127, April 02-06, 2001
• 27: Volker Weispfenning, The complexity of linear problems in fields, Journal of Symbolic Computation, v.5 n.1-2, p.3-27, February/April 1988 [doi>10.1016/S0747-7171(88)80003-8]
• 28: Volker Weispfenning, Comprehensive Gro¨bner bases, Journal of Symbolic Computation, v.14 n.1, p.1-29, July 1992 [doi>10.1016/0747-7171(92)90023-W]
• 29: Volker Weispfenning, Quantifier elimination for real algebra—the cubic case, Proceedings of the international symposium on Symbolic and algebraic computation, p.258-263, July 20-22, 1994, Oxford, United Kingdom [doi>10.1145/190347.190425]
• 30: Windsteiger, W., and Buchberger, B. Groebner: A library for computing grobner bases based on saclib. Tech. rep., RISC-Linz, 1993.

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:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms
          Subjects: Algebraic algorithms

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
Gröbner bases, constraint programming, ideals, invariant generation, program analysis, symbolic computation, verification