Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Christ, Juergen; Hoenicke, Jochen License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-27355


Instantiation-Based Interpolation for Quantified Formulae



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 | Privacy Published by LZI