Interpolation systems for ground proofs and for general proofs
Interpolation means extracting from a proof of inconsistency of A and
B a formula, called interpolant, which is implied by A,
is inconsistent with B, and only contains symbols they share.
If A and B describe system states,
an interpolant captures an intermediate state,
and therefore interpolation has applications in software model checking
and invariant generation:
- Maria Paola Bonacina and Moa Johansson.
Interpolation systems for ground proofs in automated deduction: a survey.
Journal of Automated Reasoning, 54(4):353-390, April 2015; DOI: 10.1007/s10817-015-9325-5
(preliminary versions of parts of this work were presented at the
Z3 Special Interest Group Meeting, Microsoft Research,
Cambridge, UK, November 2011, and at the
Meeting of the COST Action
Rich-model toolkit: an infrastructure for reliable computer systems (IC0901),
Torino, Italy, October 2011).
- Maria Paola Bonacina and Moa Johansson.
On interpolation in automated theorem proving.
Journal of Automated Reasoning, 54(1):69-97, January 2015; DOI: 10.1007/s10817-014-9314-0
(preliminary versions of parts of this work were presented at the
Meeting of the COST Action
Rich-model toolkit: an infrastructure for reliable computer systems (IC0901),
8th Haifa Verification Conference (HVC), Haifa, Israel, November 2012;
at the workshop Logic: Between Semantics and Proof Theory, In Honor of Prof. Arnon Avron's 60th Birthday,
School of Computer Science, Tel Aviv University, Tel Aviv, Israel, November 2012;
and at the Meeting of the COST Action Rich-model toolkit: an infrastructure for reliable computer systems (IC0901)
as 3rd Workshop on System Verification by Automated Reasoning Methods (SVARM) and
Workshop on Automation in Proof Assistants (AIPA) satellite of the European Joint Conferences on Theory and
Practice of Software (ETAPS), Tallinn, Estonia, March-April 2012).
- Maria Paola Bonacina.
Two-stage interpolation systems (Abstract).
In Proceedings of the 1st International Workshop on Interpolation: from Proofs to Applications (iPRA) satellite of the
25th International Conference on
Computer Aided Verification (CAV), Saint Petersburg, Russia, July 2013.
Technical Report, Technische Universität Wien, 2013.
- Maria Paola Bonacina and Moa Johansson.
Towards interpolation in an SMT solver with integrated superposition.
In Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT) satellite of the 23rd International Conference on Computer Aided Verification (CAV), Snowbird, Utah, USA, July 2011.
Technical Report No. UCB/EECS-2011-80, Department of Electrical Engineering and Computer Sciences, University of California at Berkeley, 9-18, 2011.
- Maria Paola Bonacina and Moa Johansson.
On interpolation in decision procedures.
In Proceedings of the Twentieth International Conference on Analytic Tableaux and Related Methods (TABLEAUX), Bern, Switzerland, July 2011.
Springer, Lecture Notes in Artificial Intelligence 6793, 1-16, 2011 (invited talk);
DOI: 10.1007/978-3-642-22119-4_1.
Maria Paola Bonacina