Non-linear Loop Invariant Generation using Grobner Bases

Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


We present a new technique for the generation of non-linear (algebraic) invariants of a program. Our technique uses the theory of ideals over the real and complex numbers to reduce the non-linear invariant generation problem to a numerical constraint solving problem. So far, the literature on invariant generation has concentrated almost exclusively on the construction of linear invariants of linear programs. There has been very 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.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Start Conference Manager
Conference Systems