Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleGenerating all polynomial invariants in simple loops
Author(s) Deepak Kapur, E. Rodríguez-Carbonell
TypeArticle in Journal
AbstractThis paper presents a method for automatically generating all polynomial invariants in simple loops. It is first shown that the set of polynomials serving as loop invariants has the algebraic structure of an ideal. Based on this connection, a fixpoint procedure using operations on ideals and Gröbner basis constructions is proposed for finding all polynomial invariants. Most importantly, it is proved that the procedure terminates in at most m + 1 iterations, where m is the number of program variables. The proof relies on showing that the irreducible components of the varieties associated with the ideals generated by the procedure either remain the same or increase their dimension at every iteration of the fixpoint procedure. This yields a correct and complete algorithm for inferring conjunctions of polynomial equalities as invariants. The method has been implemented in Maple using the Groebner package. The implementation has been used to automatically discover non-trivial invariants for several examples to illustrate the power of the technique.
KeywordsLoop invariant, Ideal of polynomials, Gröbner basis
URL http://www.sciencedirect.com/science/article/pii/S0747717107000107
JournalJournal of Symbolic Computation
Pages443 - 476
Translation No
Refereed No