Instantiation-Based Interpolation for Quantified Formulae
Juergen Christ, Jochen Hoenicke · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2010
Interpolation has proven highly effective in program analysis and verification, e. g., to derive invariants or new abstractions. While interpolation for quantifier free formulae is understood quite well, it turns out to be challenging in the presence of quantifiers. We present in this talk modifications to instantiation based SMT-solvers and to McMillan's interpolation algorithm in order to compute quantified interpolants.