Non-Linear Loop Invariant Generation using Groebner BasesSriram Sankaranarayanan , Henny Sipma, Zohar Manna |
|
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.
|
| In Principles of Programming Languages (POPL 2004) |
| © 2004, ACM: Please read copyright notification in the first page of the paper. |
| ps pdf |