Publications

Towards interpolation in an SMT solver with integrated superposition  (2011)

Authors:
Maria Paola Bonacina; Moa Johansson
Title:
Towards interpolation in an SMT solver with integrated superposition
Year:
2011
Type of item:
Contributo in atti di convegno
Tipologia ANVUR:
Contributo in Atti di convegno
Nations of authors:
SVEZIA; ITALIA
Language:
Inglese
Format:
A Stampa
Name of journal:
Technical Reports
N° Volume:
UCB/EECS-2011-80
Series:
Technical Reports
Congresso:
Ninth International Workshop on Satisfiability Modulo Theories (SMT)
Place:
Snowbird, Utah, USA
Period:
July 2011
:
DIKU, University of Copenhagen
Publisher:
DIKU, University of Copenhagen
Page numbers:
9-18
Keyword:
Theorem proving, decision procedures, satisfiability modulo theories, program checking
Short description of contents:
Interpolation is a technique for extracting intermediate formulae from a proof. It has applications in formal verification, where interpolation may enable a program analyser to discover information about intermediate program locations and states. We study interpolation in the theorem proving method DPLL(Gamma+T), which integrates tightly a superposition based prover Gamma in a DPLL(T) based SMT-solver to unite their respective strengths. We show how a first interpolation system for DPLL(Gamma+T) can be obtained from interpolation systems for DPLL, equality sharing and Gamma. We describe ongoing work on an interpolation system for Gamma, by presenting and proving complete an interpolation system for the ground case, followed by a discussion of ongoing work on an extension to the general case. Thanks to the modular design of DPLL(Gamma+T), its interpolation system can be extended easily beyond the ground case once a general interpolation system for Gamma becomes available.
Note:
The Ninth International Workshop on Satisfiability Modulo Theories (SMT) was held as a satellite of the Twenty-Third International Conference on Computer Aided Verification (CAV)
Web page:
http://profs.sci.univr.it/~bonacina/interpolation.html
Product ID:
61211
Handle IRIS:
11562/353521
Deposited On:
July 24, 2011
Last Modified:
November 2, 2016
Bibliographic citation:
Maria Paola Bonacina; Moa Johansson, Towards interpolation in an SMT solver with integrated superposition in «Technical Reports» vol. UCB/EECS-2011-80 (Technical Reports) DIKU, University of Copenhagen  in Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT) 2011DIKU, University of CopenhagenProceedings of "Ninth International Workshop on Satisfiability Modulo Theories (SMT)" , Snowbird, Utah, USA , July 2011 , 2011pp. 9-18

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo IRIS

Related projects
Title Department Managers
Integrazione di metodi di ragionamento automatico nel model checking: verifica formale automatica di sistemi di grande scala e a stati infiniti - Progetto ed integrazione di macchine di prova per l'analisi di programmi (PRIN 2007) Department Informatica Maria Paola Bonacina
<<back

Activities

Research facilities