Effectively propositional interpolants

Abstract

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.