Invariant synthesis for combined theories

Abstract. 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 in-variant templates, our algorithm reduces the invariant synthesis problem to a sequence of arithmetic constraint satisfaction queries. Since the com-bination of linear arithmetic and uninterpreted functions is a widely ap-plied 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 invari-ants over arrays and set data structures, because satisfiability questions for the theories of sets and arrays can be reduced to the theory of lin-ear arithmetic with uninterpreted functions. We have implemented our algorithm and used it to find invariants for a low-level memory allocator written in C.