Automatic generation of polynomial loop

In [17], 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 Gr¨obner 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 invar...

• Type: Conference
• Year: 2004
• Where: ISSAC
• Authors: Enric Rodríguez-Carbonell, Deepak Kapur
• Keywords: ISSAC 2004, Loop Invariants, Polynomial, Polynomial Equations