The use of interpolants in verification is gaining more and more importance. Since theories used in applica- tions are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly re-use interpolation algorithms for the component theories. We show that a sufficient and necessary condition to do this for quantifier-free interpolation is that the component theories have the ‘strong (sub-)amalgamation’ property. Then, we provide an equivalent syntactic characterization and show that such characterization covers most theories commonly employed in verification. Finally, we design a combined quantifier-free inter- polation algorithm capable of handling both convex and non-convex theories; this algorithm subsumes and extends most existing work on combined interpolation.
|Titolo:||Quantifier-Free Interpolation in Combinations of Equality Interpolating Theories|
|Parole Chiave:||interpolation, combined decision procedures|
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
|Data di pubblicazione:||2014|
|Digital Object Identifier (DOI):||10.1145/2490253|
|Appare nelle tipologie:||01 - Articolo su periodico|