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 (EUF), linear arithmetic over the rationals (LA(Q)), and some fragments of linear arithmetic over the integers (LA(Z))– 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 (UT VPI). This theory is a very useful fragment of LA(Z), 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 UT VPI, which exploits the power of modern SMT techniques. We have implemented our new algorithm within the Mat...

• Type: Conference
• Year: 2009
• Where: CADE
• Authors: Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
• Keywords: Automated Reasoning, CADE 2009, Craig Interpolant, Interpolant Generation, UT VPI