Interpolants are used in program analysis, verification and synthesis, to compute over-approximations of images, refine abstractions, or generate invariants. An interpolation system takes a proof and extracts an interpolant. Known interpolation systems use colors to track symbols in proofs. We give a color-based interpolation system for ground superposition, and then we show that the color-based approach cannot handle non-ground proofs with substitutions. We present a two-stage approach that works by tracking literals, computes a provisional interpolant, which may contain non-shared symbols, and applies lifting to obtain an interpolant. In this way we get interpolation systems for non-ground proofs by superposition and resolution.

Two-stage interpolation systems

BONACINA, Maria Paola
2013

Abstract

Interpolants are used in program analysis, verification and synthesis, to compute over-approximations of images, refine abstractions, or generate invariants. An interpolation system takes a proof and extracts an interpolant. Known interpolation systems use colors to track symbols in proofs. We give a color-based interpolation system for ground superposition, and then we show that the color-based approach cannot handle non-ground proofs with substitutions. We present a two-stage approach that works by tracking literals, computes a provisional interpolant, which may contain non-shared symbols, and applies lifting to obtain an interpolant. In this way we get interpolation systems for non-ground proofs by superposition and resolution.
Interpolation Systems; Superposition; Resolution; Satisfiability Modulo Theories; Decision Procedures
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/611552
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact