When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-27355
Go to the corresponding Portal

Christ, Juergen ; Hoenicke, Jochen

Instantiation-Based Interpolation for Quantified Formulae

Document 1.pdf (181 KB)


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.

BibTeX - Entry

  author =	{Juergen Christ and Jochen Hoenicke},
  title =	{Instantiation-Based Interpolation for Quantified Formulae},
  booktitle =	{Decision Procedures in Software, Hardware and Bioware},
  year =	{2010},
  editor =	{Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov},
  number =	{10161},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{},
  annote =	{Keywords: Interpolation Quantifier SMT}

Keywords: Interpolation Quantifier SMT
Seminar: 10161 - Decision Procedures in Software, Hardware and Bioware
Issue Date: 2010
Date of publication: 25.08.2010

DROPS-Home | Fulltext Search | Imprint Published by LZI