## Invariant Synthesis for Combined Theories

*Dirk Beyer,
Thomas A. Henzinger,
Rupak Majumdar, and Andrey Rybalchenko*

We present a constraint-based algorithm for the synthesis of
invariants expressed in the combined theory of linear arithmetic and
uninterpreted function symbols. Given a set of programmer-specified
invariant templates, our algorithm reduces the invariant synthesis
problem to a sequence of arithmetic constraint satisfaction queries.
Since the combination of linear arithmetic and uninterpreted
functions is a widely applied predicate domain for program
verification, our algorithm provides a powerful tool to statically
and automatically reason about program correctness. The algorithm
can also be used for the synthesis of invariants over arrays and set
data structures, because satisfiability questions for the theories
of sets and arrays can be reduced to the theory of linear arithmetic
with uninterpreted functions. We have implemented our algorithm and
used it to find invariants for a low-level memory allocator written
in C.

*Proceedings of the
Eighth International Conference on Verification, Model Checking, and
Abstract Interpretation*
(VMCAI),
Lecture Notes in Computer Science 4349,
Springer, 2007, pp. 378-394.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2007 Springer.