Interpolant generation for UTVPI

Abstract

The problem of computing Craig interpolants in SMT has recently received a lot of interest, mainly for its applications in formal verification. Efficient algorithms for interpolant generation have been presented for some theories of interest -including that of equality and uninterpreted functions (ε Uℱ), linear arithmetic over the rationals (LA(ℚ)), and some fragments of linear arithmetic over the integers (LA(ℤ))- and they are successfully used within model checking tools. In this paper we address the problem of computing interpolants in the theory of Unit-Two-Variable-Per-Inequality (UTVPI). This theory is a very useful fragment of LA(Zdbl;), since it is expressive enough to encode many hardware and software verification queries while still admitting a polynomial time decision procedure. We present an efficient graph-based algorithm for interpolant generation in UTVPI, which exploits the power of modern SMT techniques. We have implemented our new algorithm within the MathSAT SMT solver. Our experimental evaluation demonstrates both the efficiency and the usefulness of the new algorithm. © 2009 Springer Berlin Heidelberg.