@inproceedings{rodriguez-carbonellAutomaticGenerationPolynomial,
 title = {Automatic {{Generation}} of {{Polynomial Loop Invariants}}: {{Algebraic Foundations}}},
 author = {Rodr{\'i}guez-Carbonell, Enric and Kapur, Deepak},
 langid = {english},
 abstract = {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{\"o}bner 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.},
 year = {2004},
 booktitle = {Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation (ISSAC '04)},
 pages = {266--273},
 publisher = {ACM},
 doi = {10.1145/1005285.1005324}
}

rodriguez-carbonellAutomaticGenerationPolynomial:
  type: article
  title: 'Automatic {Generation} of {Polynomial Loop Invariants}: {Algebraic Foundations}'
  author:
  - Rodríguez-Carbonell, Enric
  - Kapur, Deepak
  date: 2004
  page-range: 266-273
  serial-number:
    doi: 10.1145/1005285.1005324
  language: en-US
  abstract: 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{ö}bner 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.
  parent:
    type: proceedings
    title: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation (ISSAC '04)
    publisher: ACM