Data di Pubblicazione:
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 delcheckers
Tipologia CRIS:
04.01 Contributo in Atti di convegno
Keywords:
Program Verification
Elenco autori:
Pettorossi, Alberto; Fioravanti, Fabio; DE ANGELIS, Emanuele; Proietti, Maurizio
Link alla scheda completa:
Titolo del libro:
22nd International Symposium on Logic-Based Program Synhesis and Transformation (LOPSTR 2012)