Leveraging Interpolant Strength in Model Checking

Craig interpolation is a well known method of abstraction successfully used in both hardware and software model checking. The logical strength of interpolants can affect the quality of approximations and consequently the performance of the model checkers. Recently, it was observed that for the same resolution proof a complete lattice of interpolants ordered by strength can be derived. Most state-of-the-art model checking techniques based on interpolation subject the interpolants to constraints that ensure efficient verification as, for example, in transition relation approximation for bounded model , counterexample-guided abstraction refinement and function summarization for software update checking. However, in general, these verification-specific constraints are not satisfied by all possible interpolants. The paper analyzes the restrictions within the lattice of interpolants under which the required constraints are satisfied. This enables investigation of the effect of the st...

• Type: Journal
• Year: 2012
• Where: CAV
• Authors: Simone Fulvio Rollini, Ondrej Sery, Natasha Sharygina
• Keywords: CAV 2012, Complete Lattice, Hardware, Manipulation Procedures, Transition Relation