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.
Titolo: | Two-stage interpolation systems |
Autori: | |
Data di pubblicazione: | 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. |
Handle: | http://hdl.handle.net/11562/611552 |
Appare nelle tipologie: | 04.02 Abstract in Atti di convegno |