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 As Get 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
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.
Subject Classification
Keywords
- Interpolation Quantifier SMT
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads