## Non-Linear Loop Invariant Generation

*Sriram 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 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.

In *Principles of Programming Languages (POPL)*, ACM, 2004.

Postscript,
PDF.
© 2004, ACM.

© Henny Sipma /
sipma@cs.stanford.edu
Last modified: Thu Jan 12 14:40:50 PDT 2004