F. Model checking software at compile time(3)

Wehaveastrongerfocusontheeffectivenessoftheanalysisandabandoninsomecasessoundnessasde nedbySteffen.Thismeans,wetreatprogramspurelyasasetofsyntacticobjectsontheprogram’sCFGandallowtocheckanyCTLpropertyonthatlevel.Whileouranalysisissoundonthissyntacticlevelitisnotnecessarilyasoundabstrac-tionoftheprogram’ssemantics.However,thisapproachhasbeenfollowedbyothers(e.g.,[12,11])andprovestobewell-suitedforcheckingreal-lifesystems.

AsimilarapproachtoourscanbefoundintheUnotool[17]anditslaterdevelopmentintoOrion[11].Theanalysisisalsodonebymodelcheckingonasyntacticlevel.However,theauthorsdonotuseanoff-the-shelfmodelchecker,butimplementmodelcheckingtechniques.Orioniscurrentlymorelimitedtocheckingforthreeproperties:uninitialisedvariables,nil-pointerdereferencesandout-of-boundsarrayindexing.Thetoolcurrentlyhasastrongfo-cusonachievingagoodsignaltonoiseratiobyincorpo-ratingsymbolicsolvertechniques.Goannafocusesonawiderrangeofproperties,withfutureplanstoincludeuser-de nedrulesandembeddedassembly.Itwillbeinterestingtocomparefutureversionsofbothtools.

Relatedtoourphilosophyis,e.g.,theworkinthestaticanalysiscommunitydonebyEngleretal.[12].Theauthorsusemeta-levelcompilation(MC)whichallowssystemim-plementorstobuildtheirownapplication-speci ccompilerextensionsbasedontheMetallanguage.Thoseextensionsareusedasspeci cationsforsearchingtheabstractsyntaxtree,control owanddata owgraph.Theapproachhasbeenfurtherdevelopedintoacommercialproduct[10].

2

Thereareothercommercialstaticanalysistools,e.g.[14,19,15,20]which,however,mostlydonotsupportspeci -cationlanguagessuchasMetalorCTL.Thislimitstheirapplicabilityforsystemdevelopment.

Asemanticmodelcheckingapproachtosoftwarever-i cationisrealisedinSLAM[1]anditssuccessorSDV,atoolusedtoverifydevicedrivers.SLAMisasuiteoftoolsforcounterexample-guidedabstractionre nement.SLAMstartswithacoarseBooleanprogramabstractionthatissubsequentlyre nedgivenpredicatesdiscoveredfromcounterexamplesintheabstraction,untilanabstrac-tionisfoundthatsatis estheproperty.Othertoolsthatim-plementcounterexample-guidedabstractionre nementareBlast[16]andMagic[4].

AtoolforboundedmodelcheckingofANSI-Ccodewaspresentedin[7].Thistool,calledCMBC,canbeusedtoverifysafetyproperties,andalsotoverifyanANSI-Cmodelofacircuitagainstaspeci cationinahardwarede-scriptionlanguagesuchasVerilog.Thetoolunrollsthepro-gramandcheckswithaSAT-solverifthereexistsanerrortraceuptothegivendepth.CMBCisparticularlyusefulfordebuggingsinceitcan ndallerrorsuptoacertaindepthquickly.

TheEauClairetool[5]makesuseofautomatictheoremproving.ItisanextendedstaticcheckerforC,basedontheearlierideasin[18].ThetooltranslatesCcodeintoasetofguardedcommandswhichwillthenbetransformedintoveri cationconditions.Theseveri cationconditionsarecheckedautomaticallybytheSimplifytheoremprover.Basedonabstractinterpretation[9]arethePoly-Space[24]andAstr´ee[3]staticanalyzers.Theyaimatprovingtheabsenceofrun-timeerrorsinprogramswrit-tenintheC/C++programminglanguages.Astr´eeanalyzesstructuredCprograms,withoutdynamicmemoryalloca-tionorrecursion.Abstractinterpretationisparticularlywellsuitedforarrayboundcheckingandalike,asitprovidesasemanticframeworktocapturedomainsandtheoperationsonthem,butsuffersfromhighcomputationalcostsresult-inginmuchlongeranalysistimes.

3SyntacticSoftwareModelChecking

Inthissectionwepresentdetailsofhowtoencodestaticanalysispropertiesbymodelcheckinginapracticalway.ThegoalistodeterminesyntacticpropertiesofC/C++pro-gramsrangingfromuninitializedvariablestonullpointerdereferences.GivenaprogramPandapropertyφthetaskofcheckingwhetherPsatis esφ,i.e.,P|=φ,isreducedtocheckingPs|=φswherePsisa nitesyntacticrepre-sentationofPandφsasyntacticencodingofφ.

Althoughweusemodelcheckingforouranalysis,thetypeofpropertiesweareaddressingaresimilartothoseinstaticanalysis.Forinstance,wecheckwhetheravariablev