We present CSIsat, an interpolating decision procedure for the quantifier-free theory of rational linear arithmetic and equality with uninterpreted function symbols. Our implementa...
A Craig interpolant of two inconsistent theories is a formula which is true in one and false in the other. This paper gives an eificient method for constructing a Craig interpolant...
Abstract. A Craig interpolant for a mutually inconsistent pair of formulas (A, B) is a formula that is (1) implied by A, (2) inconsistent with B, and (3) expressed over the common ...
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 ...
Alessandro Cimatti, Alberto Griggio, Roberto Sebas...