The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly reuse 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 interpolation algorithm capable of handling both convex and nonconvex theories; this algorithm subsumes and extends most existing work on combined interpolation. © 2014 ACM.

Quantifier-Free interpolation in combinations of equality interpolating theories / Bruttomesso, R.; Ghilardi, S.; Ranise, S.. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 15:1(2014), pp. 1-34. [10.1145/2490253]

Quantifier-Free interpolation in combinations of equality interpolating theories

Ranise S.
2014-01-01

Abstract

The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly reuse 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 interpolation algorithm capable of handling both convex and nonconvex theories; this algorithm subsumes and extends most existing work on combined interpolation. © 2014 ACM.
2014
1
Bruttomesso, R.; Ghilardi, S.; Ranise, S.
Quantifier-Free interpolation in combinations of equality interpolating theories / Bruttomesso, R.; Ghilardi, S.; Ranise, S.. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 15:1(2014), pp. 1-34. [10.1145/2490253]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333288
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 20
  • ???jsp.display-item.citation.isi??? 19
social impact