Sciweavers

DAC
2006
ACM

Automatic invariant strengthening to prove properties in bounded model checking

14 years 4 months ago
Automatic invariant strengthening to prove properties in bounded model checking
In this paper, we present a method that helps improve the performance of Bounded Model Checking by automatically strengthening invariants so that the termination proof may be obtained by analyzing shorter paths. The strengthening technique identifies sets of states as byproducts of the termination checks. It then uses SATbased preimage computations to extend those sets. Our approach may substantially speed up the verification of both failing and passing properties. We present experimental results showing that our new method improves the performance of BMC significantly. Categories and Subject Descriptors B.6.3 [Logic design]: Design aids--Verification General Terms: Verification, Algorithms
Mohammad Awedh, Fabio Somenzi
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2006
Where DAC
Authors Mohammad Awedh, Fabio Somenzi
Comments (0)