Sciweavers

Share
CAV
2012
Springer

Leveraging Interpolant Strength in Model Checking

7 years 4 months ago
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...
Simone Fulvio Rollini, Ondrej Sery, Natasha Sharyg
Added 28 Sep 2012
Updated 28 Sep 2012
Type Journal
Year 2012
Where CAV
Authors Simone Fulvio Rollini, Ondrej Sery, Natasha Sharygina
Comments (0)
books