Lifting Propositional Interpolants to the Word-Level

— Craig interpolants are often used to approximate inductive invariants of transition systems. Arithmetic relationships between numeric variables require word-level interpolants, which are derived from word-level proofs of unsatisfiability. While word-level theorem provers have made significant progress in the past few years, competitive solvers for many logics are based on flattening the word-level structure to the bit-level. We propose an algorithm that lifts a resolution proof obtained from a bit-flattened formula up to the word-level, which enables the computation of word-level interpolants. Experimental results for equality logic suggest that the overhead of lifting the propositional proof is very low compared to the solving time of a state-of-theart solver.

• Type: Conference
• Year: 2007
• Where: FMCAD
• Authors: Daniel Kroening, Georg Weissenbacher
• Keywords: FMCAD 2007, Inductive Invariants, Word-level Interpolants, Word-level Theorem Provers