Automatic generation of polynomial loop

11 years 11 months ago
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...
Enric Rodríguez-Carbonell, Deepak Kapur
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Authors Enric Rodríguez-Carbonell, Deepak Kapur
Comments (0)