×

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].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B20 Subsystems of classical logic (including intuitionistic logic)
03C40 Interpolation, preservation, definability
PDFBibTeX XMLCite
Full Text: DOI