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.

Towards interpolation in an SMT solver with integrated superposition

BONACINA, Maria Paola;
2011-01-01

Abstract

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.
2011
Inglese
STAMPA
Sì, ma tipo non specificato
UCB/EECS-2011-80
9th International Workshop on Satisfiability Modulo Theories (SMT)
Snowbird, Utah, USA
July 2011
Internazionale
contributo
Proceedings of the 9th International Workshop on Satisfiability Modulo Theories (SMT) 2011
Shuvendu Lahiri; Sanjit A. Seshia
Shuvendu Lahiri; Sanjit A. Seshia
Department of Electrical Engineering and Computer Sciences, University of California at Berkeley
9
18
10
Theorem proving; decision procedures; satisfiability modulo theories; program checking
The 9th International Workshop on Satisfiability Modulo Theories (SMT) was held as a satellite of the 23rd International Conference on Computer Aided Verification (CAV)
http://www.eecs.berkeley.edu/Pubs/TechRpts/2011/
https://mariapaola.github.io/
open
Bonacina, Maria Paola; Moa, Johansson
2
04 Contributo in atti di convegno::04.01 Contributo in atti di convegno
273
info:eu-repo/semantics/conferenceObject
File in questo prodotto:
File Dimensione Formato  
SMT-CAV2011interpolation.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 102.04 kB
Formato Adobe PDF
102.04 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/353521
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact