Pubblicazioni

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

Autori:
Maria Paola Bonacina; Moa Johansson
Titolo:
Towards interpolation in an SMT solver with integrated superposition
Anno:
2011
Tipologia prodotto:
Contributo in atti di convegno
Tipologia ANVUR:
Contributo in Atti di convegno
Nazioni degli autori:
SVEZIA; ITALIA
Lingua:
Inglese
Formato:
A Stampa
Nome rivista:
Technical Reports
N° Volume:
UCB/EECS-2011-80
Serie:
Technical Reports
Titolo del Convegno:
Ninth International Workshop on Satisfiability Modulo Theories (SMT)
Luogo:
Snowbird, Utah, USA
Periodo:
July 2011
Editore:
DIKU, University of Copenhagen
Casa editrice:
DIKU, University of Copenhagen
Intervallo pagine:
9-18
Parole chiave:
Theorem proving, decision procedures, satisfiability modulo theories, program checking
Breve descrizione dei contenuti:
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)
Pagina Web:
http://profs.sci.univr.it/~bonacina/interpolation.html
Id prodotto:
61211
Handle IRIS:
11562/353521
depositato il:
24 luglio 2011
ultima modifica:
2 novembre 2016
Citazione bibliografica:
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 CopenhagenAtti di "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

Progetti Collegati
Titolo Dipartimento Responsabili
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) Dipartimento Informatica Maria Paola Bonacina
<<indietro

Attività

Strutture