Two-stage interpolation systems

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.