Duality-based interpolation for quantifier-free equalities and uninterpreted functions

FMCAD, pp. 39-46, 2017.

Cited by: 6|Bibtex|Views24|Links
EI

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments