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 (UTVPI). This theory is a very useful fragment of LA(Z), since it is the most expressive fragment of LA(Z) with a polynomial decision procedure, and many HWand SWverification queries are naturally expressed in this fragment. 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.
Interpolant Generation for UTVPI
Cimatti, Alessandro;Griggio, Alberto;Sebastiani, Roberto
2009-01-01
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 (UTVPI). This theory is a very useful fragment of LA(Z), since it is the most expressive fragment of LA(Z) with a polynomial decision procedure, and many HWand SWverification queries are naturally expressed in this fragment. 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
