Duality-based interpolation for quantifier-free equalities and uninterpreted functions
FMCAD, pp. 39-46, 2017.
Interpolating, i.e., computing safe over-approximations for a system represented by a logical formula, is at the core of symbolic model-checking. One of the central tools in modeling programs is the use of the equality logic and uninterpreted functions (EUF), but certain aspects of its interpolation, such as size and the logical strength,...More
Full Text (Upload PDF)
PPT (Upload PPT)