Back to overview

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

Type of publication Peer-reviewed
Publikationsform Proceedings (peer-reviewed)
Author Leonardo Alt Antti Eero Johannes Hyvärinen Sepideh Asadi Natasha Sharygina,
Project Guiding SMT-Based Interpolation for Program Verification
Show all

Proceedings (peer-reviewed)

Title of proceedings 2017 Formal Methods in Computer Aided Design, {FMCAD} 2017, Vienna, Austria, October
DOI 10.23919/fmcad.2017.8102239


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, are still relatively little studied. In this paper we present a solid framework for building compact, strength-controlled interpolants, prove its strength and size properties on EUF, implement and combine it with a propositional interpolation system and integrate the implementation into a model checker. We report encouraging results on using the interpolants both in a controlled setting and in the model checker. Based on the experimentation the presented techniques have potentially a big impact on the final interpolant size and the number of counter-example-guided refinements.