Instantiation-Based Interpolation for Quantified Formulae

Christ, Juergen; Hoenicke, Jochen

License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-27355
URL: https://drops.dagstuhl.de/opus/volltexte/2010/2735/

Christ, Juergen ; Hoenicke, Jochen

Instantiation-Based Interpolation for Quantified Formulae

pdf-format:

10161.ChristJuergen.Paper.2735.pdf (0.2 MB)

Abstract

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

@InProceedings{christ_et_al:DSP:2010:2735,
  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 =		{http://drops.dagstuhl.de/opus/volltexte/2010/2735},
  annote =	{Keywords: Interpolation Quantifier SMT}
}

25.08.2010

Keywords: Interpolation Quantifier SMT

Seminar: 10161 - Decision Procedures in Software, Hardware and Bioware

Issue date: 2010

Date of publication: 25.08.2010

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