Title :
Automatic invariant strengthening to prove properties in bounded model checking
Author :
Awedh, Mohammad ; Somenzi, Fabio
Author_Institution :
Colorado Univ., Boulder, CO
Abstract :
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 SAT-based 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
Keywords :
Boolean functions; computability; formal verification; logic design; theorem proving; SAT based preimage computations; automatic invariant strengthening; bounded model checking; failing property; passing property; termination proof; Boolean functions; Data structures; Humans; Logic design; State estimation; Tellurium; Termination of employment; Algorithms; Bounded Model Checking; SAT; Verification;
Conference_Titel :
Design Automation Conference, 2006 43rd ACM/IEEE
Conference_Location :
San Francisco, CA
Print_ISBN :
1-59593-381-6
DOI :
10.1109/DAC.2006.229399