Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations

ABSTRACT

This paper presents the algebraic foundation for an approach for generating polynomial loop invariants in imperative programs. It is first shown that the set of polynomials serving as loop invariants has the algebraic structure of an ideal. Using this connection, a procedure for finding loop invariants is given in terms of operations on ideals, for which Grobner basis constructions can be employed. Most importantly, it is proved that if the assignment statements in a loop are solvable (in particular, affine) mappings with positive eigenvalues, then the procedure terminates in at most 2m+1 iterations, where m is the number of variables in the loop. The proof is done by showing that the irreducible subvarieties of the variety associated with the polynomial ideal approximating the invariant polynomial ideal of the loop either stay the same or increase their dimension in every iteration. This yields a correct and complete algorithm for inferring conjunctions of polynomial equations as invariants. The method has been implemented in Maple using the Groebner package. The implementation has been used to automatically discover nontrivial invariants for several examples to illustrate the power of the techniques.

REFERENCES

• 1: D. M. Bressoud. Factorization and Primality Testing. Springer-Verlag, 1989.
• 2: E. Cohen. Programming in the 1990s. Springer-Verlag, 1990.
• 3: M. A. Colon, S. Sankaranarayanan, and H. Sipma. Linear Invariant Generation Using Non-Linear Constraint Solving. In Computer-Aided Verification (CAV 2003), volume 2725 of Lecture Notes in Computer Science, pages 420--432. Springer-Verlag, 2003.
• 4: 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]
• 5: 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]
• 6: D. Cox, J. Little, and D. O'Shea. Ideals, Varieties and Algorithms. An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer-Verlag, 1998.
• 7: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 8: B. Elspas, M. Green, K. Levitt, and R. Waldinger. Research in Interactive Program-Proving Techniques. Technical report, Stanford Research Institute, Menlo Park, California, USA, May 1972.
• 9: P. Freire. www.pedrofreire.com/crea2_en.htm?
• 10: S. German and B. Wegbreit. A Synthesizer of Inductive Assertions. IEEE Transactions on Software Engineering, 1(1):68--75, 1975.
• 11: Tony Hoare, The verifying compiler: A grand challenge for computing research, Journal of the ACM (JACM), v.50 n.1, p.63-69, January 2003 [doi>10.1145/602382.602403]
• 12: Anne Kaldewaij, Programming: the derivation of algorithms, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 13: M. Karr. Affine Relationships Among Variables of a Program. Acta Informatica, 6:133--151, 1976.
• 14: Shmuel Katz , Zohar Manna, Logical analysis of programs, Communications of the ACM, v.19 n.4, p.188-206, April 1976 [doi>10.1145/360032.360048]
• 15: Donald E. Knuth, The art of computer programming, volume 2 (3rd ed.): seminumerical algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1997
• 16: M. Müller-Olm and H. Seidl. Computing Interprocedurally Valid Relations in Affine Programs. In ACM SIGPLAN Principles of Programming Languages (POPL 2004), pages 330--341, 2004.
• 17: E. Rodríguez-Carbonell and D. Kapur. Program Verification Using Automatic Generation of Polynomial Invariants. \tt www.lsi.upc.es/\ erodri.
• 18: 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
• 19: R P Stanley, Enumerative combinatorics, Wadsworth Publ. Co., Belmont, CA, 1986
• 20: Ben Wegbreit, The synthesis of loop predicates, Communications of the ACM, v.17 n.2, p.102-113, Feb. 1974 [doi>10.1145/360827.360850]
• 21: B. Wegbreit. Property Extraction in Well-founded Property Sets. IEEE Transactions on Software Engineering, 1(3):270--285, September 1975.

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

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Algorithms, Verification

Keywords:
groebner basis, ideal, loop invariant