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
Theorem proving; decision procedures; satisfiability modulo theories; program checking
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