Details:

Title
Author(s)	Zohar Manna, Sriram Sankaranarayanan, Henny B. Sipma
Text	Also appeared in ACM SIGPLAN Notices, Vol. 39, Issue 1 (January 2004)
Type	Article in Conference Proceedings
Abstract	We 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.
Keywords
Length	12
ISBN	1-58113-729-X
File
Language	English
Pages	318-329
Publisher	ACM Press
Address	New York, NY, USA
Year	2004
Translation	No
Refereed	No
Organization	Stanford University
Conferencename	Annual Symposium on Principles of Programming Languages