Drews, Samuel; Albarghouthi, Aws Effectively propositional interpolants. (English) Zbl 1411.68063 Chaudhuri, Swarat (ed.) et al., Computer aided verification. 28th international conference, CAV 2016, Toronto, ON, Canada, July 17–23, 2016. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 9780, 210-229 (2016). Summary: We present a novel interpolation algorithm for effectively propositional logic (epr), a decidable fragment of first-order logic that enjoys a small-model property. epr is a powerful fragment of quantified formulas that has been used to model and verify a range of programs, including heap-manipulating programs and distributed protocols. Our interpolation technique samples finite models from two sides of the interpolation problem and generalizes them to learn a quantified interpolant. Our results demonstrate our technique’s ability to compute universally-quantified, existentially-quantified, as well as alternation-free interpolants and inductive invariants, thus improving the state of the art.For the entire collection see [Zbl 1342.68011]. Cited in 1 Document MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 03B20 Subsystems of classical logic (including intuitionistic logic) 03C40 Interpolation, preservation, definability PDFBibTeX XMLCite \textit{S. Drews} and \textit{A. Albarghouthi}, Lect. Notes Comput. Sci. 9780, 210--229 (2016; Zbl 1411.68063) Full Text: DOI