Search Results

Documents authored by Hoenicke, Jochen


Document
Instantiation-Based Interpolation for Quantified Formulae

Authors: Juergen Christ and Jochen Hoenicke

Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)


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.

Cite as

Juergen Christ and Jochen Hoenicke. Instantiation-Based Interpolation for Quantified Formulae. In Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, Volume 10161, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@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/entities/document/10.4230/DagSemProc.10161.4},
  URN =		{urn:nbn:de:0030-drops-27355},
  doi =		{10.4230/DagSemProc.10161.4},
  annote =	{Keywords: Interpolation Quantifier SMT}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail