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

• Type: Conference
• Year: 2006
• Where: DAC
• Authors: Mohammad Awedh, Fabio Somenzi
• Keywords: DAC 2006, Design Automation, Technique Identifies Sets, Termination Checks, Termination Proof