Wepresentametho dforverifyingprop ertiesofimp erativeprogramsbyusingtechniquesbasedonconstraintlogicprogramming(CLP).Weconsiderasimpleimp erativelanguage,calledSIMP,extendedwithanondeterministicchoiceop eratorandweaddresstheproblemofcheckingwhetherornotasafetyprop erty?(thatsp eciesthatanun-safecongurationcannotb ereached)holdsforaSIMPprogramP.Theop erationalsemanticsofthelanguageSIMPissp eciedviaaninter-preterIwrittenasaCLPprogram.Therstphaseofourvericationmetho dconsistsinsp ecializingIwithresp ecttoP,therebyderivingasp ecializedinterpreterIP.Then,wesp ecializeIPwithresp ecttotheprop erty?andtheinputvaluesofP,withtheaimofderivingapro-gramwhoseleastmo delcanb ecomputedasanitesetofconstrainedfacts.Tothispurp oseweintro duceanovelgeneralizationstrategywhich,duringsp ecialization,preservesthesocalledbranchingb ehaviourofthepredicatedenitions.Wehavefullyautomatedourmetho dandwehavemadeitsexp erimentalevaluationonsomeexamplestakenfromtheliter-ature.Theevaluationshowsthatourmetho discomp etitivewithresp ecttostate-of-the-artsoftwaremo delcheckers
Branching Preserving Specialization for Software Model Checking
De Angelis E;Fioravanti F;Pettorossi A;Proietti M
2012
Abstract
Wepresentametho dforverifyingprop ertiesofimp erativeprogramsbyusingtechniquesbasedonconstraintlogicprogramming(CLP).Weconsiderasimpleimp erativelanguage,calledSIMP,extendedwithanondeterministicchoiceop eratorandweaddresstheproblemofcheckingwhetherornotasafetyprop erty?(thatsp eciesthatanun-safecongurationcannotb ereached)holdsforaSIMPprogramP.Theop erationalsemanticsofthelanguageSIMPissp eciedviaaninter-preterIwrittenasaCLPprogram.Therstphaseofourvericationmetho dconsistsinsp ecializingIwithresp ecttoP,therebyderivingasp ecializedinterpreterIP.Then,wesp ecializeIPwithresp ecttotheprop erty?andtheinputvaluesofP,withtheaimofderivingapro-gramwhoseleastmo delcanb ecomputedasanitesetofconstrainedfacts.Tothispurp oseweintro duceanovelgeneralizationstrategywhich,duringsp ecialization,preservesthesocalledbranchingb ehaviourofthepredicatedenitions.Wehavefullyautomatedourmetho dandwehavemadeitsexp erimentalevaluationonsomeexamplestakenfromtheliter-ature.Theevaluationshowsthatourmetho discomp etitivewithresp ecttostate-of-the-artsoftwaremo delcheckersI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
