License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.10161.4
URN: urn:nbn:de:0030-drops-27355
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2735/
Go to the corresponding Portal

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:DagSemProc.10161.4,
  author =	{Christ, Juergen and Hoenicke, Jochen},
  title =	{{Instantiation-Based Interpolation for Quantified Formulae}},
  booktitle =	{Decision Procedures in Software, Hardware and Bioware},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10161},
  editor =	{Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2010/2735},
  URN =		{urn:nbn:de:0030-drops-27355},
  doi =		{10.4230/DagSemProc.10161.4},
  annote =	{Keywords: Interpolation Quantifier SMT}
}

Keywords: Interpolation Quantifier SMT
Collection: 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