DagSemProc.10161.4.pdf
- Filesize: 181 kB
- 12 pages
Document
Instantiation-Based Interpolation for Quantified Formulae
Authors
-
Part of:
Volume:
Dagstuhl Seminar Proceedings, Volume 10161
Series: Dagstuhl Seminar Proceedings (DagSemProc) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2010-08-25
Cite AsGet BibTex
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)
https://doi.org/10.4230/DagSemProc.10161.4
https://doi.org/10.4230/DagSemProc.10161.4
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.
Keywords
- Interpolation Quantifier SMT
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads