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


TitleNon-linear loop invariant generation using Gröbner bases
Author(s) Zohar Manna, Sriram Sankaranarayanan, Henny B. Sipma
TextAlso appeared in ACM SIGPLAN Notices, Vol. 39, Issue 1 (January 2004)
TypeArticle in Conference Proceedings
AbstractWe present a new technique for the generation of non-linear (algebraic) invariants of a program. Our technique uses the theory of ideals over polynomial rings to reduce the non-linear invariant generation problem to a numerical constraint solving problem. So far, the literature on invariant generation has been focussed on the construction of linear invariants for linear programs. Consequently, there has been little progress toward non-linear invariant generation. In this paper, we demonstrate a technique that encodes the conditions for a given template assertion being an invariant into a set of constraints, such that all the solutions to these constraints correspond to non-linear (algebraic) loop invariants of the program. We discuss some trade-offs between the completeness of the technique and the tractability of the constraint-solving problem generated. The application of the technique is demonstrated on a few examples.
KeywordsGröbner bases, constraint programming, ideals, invariant generation, program analysis, symbolic computation, verification
PublisherACM Press
AddressNew York, NY, USA
Translation No
Refereed No
Organization Stanford University
ConferencenameAnnual Symposium on Principles of Programming Languages