General  Information
Important Dates
Conference Poster
Organizing Committee
Program and Schedule
Invited Talks
Contributed Talks
Software Exhibitions
Registered Participants
 Call  For
Research Papers
Software Exhibitions
Jenks Prize Nominations
 Local  Information
Conference Location
Speakers' Information
Gastronomic Guide
Additional Information
Social Events
Previous ISSACs
Other Events



Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations

E. Rodriguez-Carbonell, D. Kapur


In [rodrikapurIJCAR03], an abstract framework for automatically generating loop invariants of imperative programs was proposed. This framework was then instantiated for the language of conjunctions of polynomial equations for expressing loop invariants. This paper presents an algebraic foundation of the approach. It is first shown that the set of polynomials serving as loop invariants has the algebraic structure of an ideal. Using this connection, it is proved that the procedure for finding invariants can be expressed using operations on ideals, for which Groebner 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 changing in the loop. The proof is done by showing that the irreducible subvarieties of the variety associated with a 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 technique.

  issac2004 @