Automatic Invariant Strengthening toProveProperties inBoundedModelChecking* MohammadAwedh
Fabio Somenzi · 2006
WithSATsolvers, theclassical approach isfollowed: Onefirst Inthis paper, wepresent amethod that helps improve theperfor-checks thesatisfiability oftheconjunction oftheinitial states and manceofBounded ModelChecking byautomatically strengthen- thebadstates. Ifthat conjunction isunsatisfiable, onethenchecks inginvariants sothat thetermination proof maybeobtained byan- forsatisfiability thetransition relation ofthemodelwhenthepresent alyzing shorter paths. Thestrengthening technique identifies sets state isconstrained tosatisfy theinvariant andthenextstate isconofstates asbyproducts ofthetermination checks. Itthen usesSAT- strained toviolate it. Anegative result proves theinductive step. based preimage computations toextend those sets. Ourapproach Inductive invariants areamongtheeasiest toprove, but, inmany maysubstantially speed uptheverification ofboth failing andpass- cases onehastodeal withnoninductive invariants. Inthat case one ingproperties. Wepresent experimental results showing that our mayuseanauxiliary invariant, chosen insuchawaythat its connewmethod improves theperformance ofBMC significantly.junction withthegiven invariant makesitinductive. Ifonechooses theauxiliary invariant soastoleave outtheunreachable goodstates Categories andSubject Descriptors with badsuccessors, oneobtains aconjunction onwhich theinducB.6.3 [Logic design]: Design aids-Verification tive step will succeed. General Terms: Verification, Algorithms Onecanleave ittotheuserofthemodelchecker tosupply the