Program analysis as model checking of abstract interpretations

AbstractInterpretations

DavidSchmidt

KansasStateUniversity

󰀐

BernhardSteffen

(USA)

Universit¨atDortmund󰀐󰀐(D)

Abstract.Thispaperpresentsacollectionoftechniques,amethodology,

inwhichabstractinterpretation,flowanalysis,andmodelcheckingareemployedintherepresentation,abstraction,andanalysisofprograms.Themethodologyshowstheareasofintersectionofthedifferenttech-niquesaswellastheopportunitesthatexistwhenonetechniqueisusedinsupportofanother.Themethodologyispresentedasathree-steppro-cess:First,froma(small-step)operationalsemanticsdefinitionandaprogram,oneconstructsaprogrammodel,whichisastate-transitionsys-temthatencodestheprogram’sexecutions.Second,abstractionupontheprogrammodelisperformed,reducingthedetailofinformationinthemodel’snodesandarcs.Finally,theprogrammodelisanalyzedforpropertiesofitsstatesandpaths.

1Motivation

Recentresearchsuggeststhattheconnectionsbetweeniterativedata-flowanalysisandmodelcheckingareintimate.Themoststrikingapplicationistheuseofamodelcheckertocalculateiterativebit-vector-baseddata-flowanalyses[44,47–49];thisapplicationdependsontheencodingofthebit-vector’sbitsasbooleanpropositionswhicharedecidedbymodelchecking.

Buttheapplicationofamodelcheckerastheengineforflowanalysisiswiderthanbit-vectorproblemsonsequentialprograms.RecentworkbySteffenandhiscolleagueshasadaptedthebasicconstructiontoanefficienttreatmentofparallelprograms[29],andworkbyDwyerandothers[19–21]showshowproblemsformallysolvedwithdata-flowanalysistechniquesaremoresimplyexpressedandsolvedbymodel-checkingtechniques.Andtherearenumerousexamplesofprogramvalidationdonewithflowanalysisthatinthepresentdaywouldbetermedmodelchecking[5,6,33,34,39,40].

Tounderstandtheconnectionsbetweenflowanalysisandmodelchecking,athirdcomponent,abstraction,moreprecisely,abstractinterpretation,mustbeused.Abstractinterpretationprovidesthefoundationuponwhichsafeprogramrepresentationsrest,andunderstandingwhymodelcheckingisapropercompu-tationaltoolforflowanalysisdependsuponanunderstandingoftheunderlyingabstractiontechniques.

Thepurposeofthispaperistointroduceacollectionoftechniques,perhapsamethodology,inwhichabstraction,flowanalysis,andmodelcheckingareem-ployedintherepresentation,abstraction,andanalysisofprograms.Themethod-ologyismeanttoshowtheareasofintersectionofthedifferenttechniquesaswellastheopportunitesthatexistwhenonetechniqueisusedinsupportofanother.Themethodologyisbasedonathree-stepprocess:First,froma(small-step)operationalsemanticsdefinitionandaprogram,oneconstructsaprogrammodel,whichisastate-transitionsystemthatencodesone(ormany,orall)ofthepro-gram’sexecutions.Second,onemightabstractupontheprogrammodel,reducingthedetailofinformationinthemodel’snodesandarcs.Finally,oneanalysesthemodelforpropertiesofitspaths,e.g.,livevariablesinformation,redundancyinformation,safetyproperties,etc.Themethodsusedwithinthethreestagesin-cludeabstractinterpretation,flowanalysis,andmodelchecking.Insomeplacesthetoolsareinterchangeable;inothers,onetoolclearlyplaysasingularrole.Thepaperisstructuredasfollows:reviewsofiterativedataflowanalysisandmodelcheckingareundertakenfirst.Next,theabstractinterpretationofoperationalsemanticsdefinitionsisreviewed,anditisshownhowtoconstructprogrammodels.Followingthis,abstractiononprogrammodelsispresented.Correctnessissuesarereviewed,andfinally,theextractionofprogrampropertieswithintheframeworkisexamined.Thepaperconcludeswithabrieflookatextensionstothebasictechnique.

2IterativeFlowAnalysis

EntitiesofObservation

Data-flowinformationcanbeconsideredan“entityofobservation”;thesetofsuchentitiesistypicallystructuredasacompletelattice,wheretheorderingontheelements,󰀝,modelstheprecisionofinformationwhere‘smaller’meansmoreprecise,andthelatticeoperations󰀛and󰀜constructleastupperboundsandgreatestlowerboundsofarbitrarysubsets.Inthispaperwetypicallyassumealatticestructureforsetsofentitiesofobservation.ProgramModels

Atraditionaliterativedata-flowanalysisworksfromaprogram’scontrol-flowgraph,whichisoneinstanceofaprogrammodel:AprogrammodelPisa5-tuple(S,A,→,s,E),where1.Sisasetofnodesorprogramstates.

p1

¬evenxp3y:=2

evenx

p2

x:=xdiv2

p4

IterativeDataFlowAnalyses

Givenaprogrammodel,onecandefineuponitaniterativedata-flowanalysisbydefiningalatticeofentitiesofobservation,andforeachtransitionintheprogrammodel,atransferfunction.Oneusesthelatticeandfunctionstodefineasetofequations,oneperprogrampoint(orstate)inthemodel.Solutionoftheequationsyieldsthedesireddata-flowinformation.Weclassifydata-flowanalysesasbeingeitherforwardsorbackwards1andasbeingeither󰀛-or󰀜-based.

Insimpleterms(see[25,28]foraformaldefinition),onedefinesabackwards-󰀛data-flowanalysisofaprogrammodelbymeansof

–asetofentitiesofobservation,D,partiallyorderedasacompletelattice.–foreachA∈A,atransferfunction,fA:D→D,thatismonotoniconD:ford,d󰀆∈D,d󰀝d󰀆impliesfA(d)󰀝fA(d󰀆).2–foreachprogramstate,p∈S,aflowequation,

󰀄

valp={fA(valq)|(p,A,q)∈→}

Theadequatesolutiontothesetofflowequationscanbedeterminedbyaleastfixed-pointcomputation.

Similarly,onecandefineabackwards-󰀜-flowanalysisbyreplacingthepreviousoccurrenceof󰀛by󰀜andcomputingthegreatest-fixed-pointsolutionoftheequations.Finally,onecandefineaforwardsanalysisbyswappingtheoccurrencesofvalpandvalqintheflowequationscheme.

Oneexampleofabackwards-󰀛data-flowanalysisislive-variablesanalysisonacontrol-flowgraph,whichisformalizedby

Var

–D=2,whereVaristhecollectionoftheprogram’svariables;

–fA(s)=UsedInA∪(notModifiedInA∩s),whereUsedInAdefinesthosevari-ablesreferencedinactionA,andnotModifiedInAdefinesthosevariablesthatarenotmodified(assignedto)inA.Theflowequationsfollowfromtheaboveinformation.Figure2showsthelivevariablesanalysisfortheprogrammodelinFigure1.

3ModelChecking

Modelcheckingisemployedtovalidatepropertiesoffinite-stateprogrammodels.Thisscopeissufficientforthepurposesofthispaper,butinterestedreadersarereferredto[4]fortechniquescoveringinfinitestatemodelsthatexplicitlymodelinterproceduralstructure.Theconsideredpropertiesarelogicalpredicates

Fig.2.Flowequationsandsolutionforlive-variablesanalysis

thattypicallydiscussdependenciesbetweenoccurrencesofspecificactionswithinpathsinthemodel,e.g.,“allpathsstartingfromthecurrentprogrampointeventuallyincludeanaaction”or“thereexistsapathincludinganaactioninfinitelyoften.”TheSyntax

Asalogicforspecifyingstaticanalysisalgorithms,wewillconsideravariantofthetemporallogicCTL[7]thatincludesaparameterizedversionofthe“Hence-forth”operator,thekeyforspecifyingqualifiedsafetyproperties.Thislogicisparticularlysuitedforexpressingpropertiesofstateswithinagiven(program)model.

Thelogic’ssyntaxisparameterizedonadenumerablesetBofatomicpropo-sitions3onstatesandacompletelatticeofactionsA.LetβrangeoverBandA⊆A:

Φ::=β|Φ∧Φ|¬Φ|[A]Φ|

AGAΦ|

Wewritep|=ΦtodenotethatpropositionΦholdstrueatstatep,andwesaythatpsatisfiesΦ.TheSemantics

SatisfactionisdefinedwithrespecttoagivenprogrammodelPcontainingpaccordingtothefollowingintuition:p|=βisassumedtobedecidable,p|=Φ1∧Φ2ifpsatisfiesbothΦ1andΦ2.p|=¬ΦifpdoesnotsatisfyΦ,andp|=[A]Φifeveryoneofp’sA-successorstatessatisfiesΦ.Notethatthisimpliespsatisfies[A]ffexactlywhenphasnoA-successors.Analogously,psatisfies

[A]ffexactlywhenphasnoA-predecessors.Finally,p|=AGAΦifΦholdsineverystatereachablefrompviaA-transitions,anditsatisfies

3

Inthispaperwesimplyconsiderthreeatomicpropositions,tt,start,andend,whichcharacterizethesetofallstates,thestartstateandthesetofendstates,respectively.Ingeneral,anysetofdecidablecharacterizationsofsetsofstatescouldbetaken.

Remark:ThedifferencebetweenthestandardHenceforthoperatorAGΦandtheparameterizedversionAGAΦiswithrespecttoreachability:Forp|=AGΦtohold,allstatesreachablefromalltransitionsfrompmustsatisfyΦ,whereasforp|=AGAΦ,onlythosestatesreachedfrompbytraversingtransitionslabelledbyanactionfromAmustsatisfyΦ.

Theformalsemanticdefinitionofthelogicderivedfromthemodalµ-calculuscanbefoundin[47].

[A].Moreover,asInthefollowingwewillwrite[.]or

usual,wecandefinethefollowingdualstotheoperatorsofourlanguageandtheimplicationoperator⇒by:

ff=¬tt

Φ1∨Φ2=¬(¬Φ1∧¬Φ2)󰀟A󰀗Φ=¬[A](¬Φ)

[A](¬Φ)

TheApplication

Acrucialconnectionbetweeniterativedata-flowanalysisandmodelcheckingwasdemonstratedbySteffen[47,48],whonotedthesimilaritiesbetweencomputingtheresultsofasetofdata-flowequationsandcomputingthesetofstatesthatsatisfiedamodalmu-calculusspecification.Forexample,theequationschemethatcomputeslivevariables,

󰀁

Livep={UsedIna∪(notModifiedIna∩s)|source(a)=p}

EFAΦ=¬AGA¬Φ

AGA¬Φ

Φ⇒Ψ=¬Φ∨Ψ

canbetransliteratedintothefollowingformulaofourlogicthatexpressesswhetheravariable,x,isliveataprogrampoint:

isLivex=EF{a|a=modx}󰀟usex󰀗tt

Thisformulationisbasedonabstractionsoftheactionsthatannotatethearcsofaprogrammodel:Assignmentstatements,v:=e,areabstractedtoactionsoftheform,modvanduseu,forthosevariables,u,usedine;tests,e,areabstractedtoactionsuseu,forthosevariables,u,usedine.

Whenonemodelcheckstheassertions,p|=isLivex,forallvariablesx,oneineffectcomputesthebit-vectorsolutionfortheflowequationLivep.Astan-darditerativemodelcheckerwoulddothis,e.g.,forthevariablexofFigure1byinitially‘marking’allthestatesoftheprogrammodelsatisfying󰀟usex󰀗ttwith‘true’,and,subsequently,stepwiselyspreadingthisinformationtoallstateshavinga{a|a=modx}-successorbeingmarked‘true’untilafixedpointisreached,i.e.,nofurtherstatecanbemarked‘true’accordingtothedescribedrules.Fortheconsideredexampleprogramthefixedpointisreachedalreadybytheinitializationprocedure.

Technically,formulaeofthelogicconsideredherewouldbefirsttranslatedintomodalequationalsystems[10],acompactrepresentationofthemodalµ-calculus,

whichhavetheappropriategranularitytodirectlysteerthefixpointcomputationprocess.isLivexwouldbetranslatedintothefollowingmin-equation4

MIN:

isLivex=󰀟usex󰀗tt∨󰀟{a|a=modx}󰀗isLivex

Thefixpointcomputationneedsonebitforeachsuchequation.Inparticular,

asexpected,onebit(perprogramvariable)issufficientforcheckinglivenessofvariables.

WhySafetyProperties

Inthispaper,wewillexploretheconnectionbetweenflowanalysisandmodelcheckingwhilefocussingonthepreservationofsafetyproperties,i.e.propertieswhichareguaranteedtoholdforallreachablestates.Inotherwordstheseprop-ertiesarecharacterizedbyholdingeverywherealongallprogramexecutions,andthereforecorrespondtothepropertieswhichcanbespecifiedusingtheparame-terizedHenceforthoperatorAGx.

isLivexisnotasafetyproperty,asitquantifiesexistentiallyovertheexecu-tionpaths5aswellasoverthestatesofagivenexecution.6However,thiscausesnorealharm,asoneisnotinterestedinthefactwhetheravariableislive,butinthecomplement,asthedetectionofdeadvariablesisakeyfordead-codeelimination,andthispropertyisindeedasafetyproperty.Andindeed,aspro-gramtransformationsmustbecorrectforallpossibleprogramexecutions,itisclearthattheymustbebaseduponinformationwhichishorizontallyuniversallyvalid.Incontrast,thereseemtoberelevantproblems,likee.g.downsafety[30],i.e.,thepropertythatacertainexpressionwillbeexecutedineverycontinu-ationoftheprogram,whichseemtoaskforexistentialverticalquantification.Surprisingly,alsothesepropertiestypicallycanbebetterformulatedasa(pa-rameterized)safetypropertythanasalivenessproperty.Thisisduetothefactthattheprogramexecutionsweareinterestedinaretypicallyterminatingpro-gramexecutions.E.g.,fordownsafety,wedonotrequiretheexpressiontobeexecutedonpaths‘starving’inaloop,7butonlyonthosewhichreachtheendpointoftheprogram.8Thispropertycanreadilybeexpressedwithasinglepa-rameterizedHenceforthoperator,ifweassumethattheendpointoftheprogramischaracterizedbytheatomicpropositionend:

AG{a|a=usex}(¬end∧󰀟modx󰀗ff)

c1;c2,σ−→c2,σ󰀄

c

󰀄

c1,σ−→c󰀄1,σ

c

[e]σ⇒false

ifethenc1elsec2fi,σ−→c1,σ

e

Fig.3.Small-stepsemanticsforimperativelanguage

Technically,wewillpresentasimulation-basedcriterionforguaranteeingsafety,

whichbridgesthegapbetweentheoperationalsemanticsofaprogrammodelondifferentlevelsofabstraction.

4OperationalSemanticsandAbstractions

Ourdefinitionofprogrammodelincludesnotonlycontrol-flowgraphsbutalsoexecutiontraces,theirabstractinterpretations,behaviourtrees,andotherkindsofabstracttransitionsystems.Indeed,aprogram’scontrol-flowgraphcanbesimplyregardedasaprogrammodelarisingfromanabstractinterpretationoftheprogram’ssemantics,wheretheprogram’sstoreisabstractedtonil.Small-StepStructuralOperationalSemantics

Weassumethataprogramminglanguagecomeswithasmall-stepstructuraloperationalsemantics.AnexampleofsuchasemanticsappearsinFigure3.Itisconvenienttolabeleachtransitionwiththeprimitivecommand/expressionthatgeneratesthetransition.

Figure4displayspartoftheoperationalsemanticsoftheprograminFigure1generatedfromthesmall-stepsemanticsrules.Wecallthederivationinthefigureaconcretecomputation.Notethattheconcretecomputationisalsoaprogrammodel.

Fig.4.Concretecomputation

StandardModels

Givenaprogramminglanguagewithasmallstep-semantics,thestandardpro-grammodellooksasfollows:

–programstatesaretheconfigurationsappearingbetweentransitionsteps(e.g.,programpoint,storepairs,(p,σ))

–actionsaretheelementarystatementsandexpressionsofthelanguage.

–transitionsaredefinedbythesmallstepsandarelabeledwiththecorre-spondingprimitivecommand/expression.

–thestartstateistheinitialconfiguration,andtheendstatesarethosestateshavingnosuccessor.Aswewillsee,thesestandardmodelsfullycomprisethecomputationsassociatedwithasmall-stepsemantics.Infact,aconcretecomputationandthecorrespond-ingstandardprogrammodelaremutualsimulationsofeachotherintheformalsenseestablishedinSection5.Thustheyaresemanticallyfullyinterchangeableforthepurposesconsideredhere,andarethereforeaconvenientabstractprogramrepresentation.

AbstractInterpretation

Forstaticanalysispurposes,wewishtogenerateafiniteprogrammodelthatcomprisesallrelevantconcreteoperationalsemanticsexecutions.Todothis,weemploytheabstractinterpretationmethodologyofCousotandCousot[14–16]:Wereplacetheconcretedomains,ValandStore,byabstractdomains,AbsValandAbsStore,andwecomputeaprogram’soperationalsemanticswiththenewdomainstoarriveatthecorrespondingprogrammodel.Foreaseofexposition,werequirethattheabstractdomainsbecompletelattices.Withtheappropriatenotionofabstractionofoperations,theabstractdomainswillgenerateabstractprogrammodelsthatsimulatethecorrespondingconcretecomputationmodels(cf.Section5).GaloisConnections

Toprovethesimulationproperty,onemustrelatetheabstracttoconcretedatadomainsbymeansofGaloisconnections9[14].Ifwethinkofanabstractdatadomain,AbsVal,asthe“entitiesofobservation,”thenwemustestablishwhichsubsetofValisdenotedbyan“entity”a∈AbsVal.Wedosowithamonotone

Val

mapping,aconcretizationfunction,γ:AbsVal→2.Ofcourse,thereshould

Val

beaninversecorrespondence,amonotoneα:2→AbsVal,theabstractionfunction;inparticular,α({c})identifiestheelementinAbsValthat“represents”c∈Val.Wedesirethat(α,γ)formaGaloisconnection,becausethisimpliesα({c})=󰀜{a|c∈γ(a)}.ItiswellknownthatoneadjointofaGaloisconnectionuniquelydeterminestheother.

Ausefulintuitionisthatγdefinesabinary“simulation”relation:forc∈Val,a∈AbsVal,csafeaiffc∈γ(a).Thatis,cissimulatedorsafelyapproximatedbya.Further,itispossibletobeginwiththebinaryrelation,safe,anddefineaGaloisconnectionfromit:IfsafeisisbothU-closed,i.e.,csafea1anda1󰀝a2implycsafea2,andG-closed,i.e.,c󰀆safe󰀜A,whereA={a󰀆|c󰀆safea󰀆},thenoneobtainsaGaloisconnection[43].

Becauseoftheseequivalences,wedefineaGaloisconnectionbyanyoneofaγ,α,orUG-closedrelationinthesequel.ControlFlowGraphs

Hereistheabstractionforcontrol-flowgraphs:

AbsVal={nil}

AbsStore=Identifier→AbsVal={nil}

γ:AbsValue→2γ(nil)=Val

Store

γ:AbsStore→2γ(nil)=Store

Val

p1,nil

¬evenxp3,nil

y:=2

evenxp2,nil

x:=div2

nil

Inthecaseofeven-oddanalysis,theabstractionofthesuccessoroperation,succ(n)=n+1,isnaturallyapproximatedbythisfunction:

succ(o)⇒esucc(e)⇒o

succ(󰀘)⇒󰀘succ(⊥)⇒⊥

Sometimes,imprecisioncanariseduetoabstraction;considertheabstractversionofdivisionby2,whichproducesananswerof󰀘whenaneven-orodd-valuednumberisdividedby2:

div2(⊥)⇒⊥

div2(a)⇒󰀘,foralla∈{e,o,󰀘}

AbstractOperationalSemantics

Oneusestheproved-safeabstractoperationstodefineasmall-stepsemanticsforgeneratingabstractprogrammodels.Theintuitionisthatoneinstantiatestheruleschemestousetheabstractoperationsratherthantheconcreteones.Then,oneusestheinstantiatedrulestogenerateaprogrammodel.Butastandardproblemisdecidingthetestsofconditionalcommands.(Forexample,howdoestheeven-oddanalysisdecidethetestoftheconditionalcommandinthisexample:x:=xdiv2;ifevenxthenc1elsec2fi?)Asolutionistorewritetherulesfortheconditionalasfollows:

[e]σ⇒v,true󰀝v

ifethenc1elsec2fi,σ−→c2,σ

ThisformatassumesthattheconcreteBooleandomainisabstractedtoalattice,{⊥,true,false,󰀘}.Ifonewishestoretaintheformatoftheoriginalsmall-stepruleschemes(andnotperformabstractiononBoolean),thenonemustutilizerelationaldefinitionsofabstractoperations.10Butthistopicwillnotbedevelopedfurtherinthispaper.

Whenweuseabstractsemanticsruleschemeslikethetwoabove,theprogrammodelscontainnondeterministicbranching(aswouldbethecaseintheexampleprogram,x:=xdiv2;ifevenxthenc1elsec2fi),becausetheoutcomeofthetestexpressionofaconditionalcommandmightnotbeuniquelytrueorfalse.Figure6showstwoabstractprogrammodelsgeneratedfromtheeven-oddabstractionfortheprograminFigure4.Thefirstprogrammodelshowstheresultofanalyzingaprogramwherexstartsasodd-valued;thesecondmodelresultswhenxstartsaseven-valued.Theexamplesshowthatmorepreciseinformationaboutprogrampathscanbeelicitedthanwhatoneobtainsfromacontrol-flowgraph.Suchmodelsmightbeusediftemporalpropertiesoftheprogram’spathsmustbevalidated,oriftheinputstoaprogramarerestrictedtoaparticularrange(e.g.,inputxisrestrictedtobeodd-valued),orifbetterqualitycodecanbe

¬e

p1,σo,󰀁¬evenx

p1,σe,󰀁evenx

p3,σo,󰀁y:=2p3,σo,e

p2,σe,󰀁

x:=xdiv2

p1,σ󰀁,󰀁

evenx

¬evenxp3,σ󰀁,󰀁

y:=2

p2,σ󰀁,󰀁

x:=xdiv2

σ󰀁,e

5Simulations

Onestepofthe“globalization”oftheabstractionofaprogrammodelistheabstractionoftheactionsthatlabelthearcsofthemodel.Inthefollowing,wewillfirstintroduceabstractiononactionsbymeansoftheprominentUse-Modabstraction,andafterwardswewillconsiderthecorrectnessofsuchabstractionsrelativetotheproofsofcorrectnessoftheabstractionsondatadomainsandoperations.

AbstractionofActions

Thedevelopmentintheprevioussectionsofabstractionofdatadomainsandoperationsisstandard.Butwecanabstractonsourceprogramsyntaxaswell,moreprecisely,wecanabstractontheactionsthatlabelthearrowsofaprogrammodel

OneexampleofabstractionofactionsisthereplacementofacommandorexpressionbyitsUse-Modinformation.Forexample,theUse-Modabstractionofthecommand,x:=x+y,wouldbe{modx,usex,usey},andtheabstractionoftheexpression,evenx,wouldbe{usex}.

HereisaformalizationofUse-Modabstraction;becauseUse-valuesarefun-damentallycovariantandMod-valuesarefundamentallycontravariant,wemusttakecareinformulatingthelattice,UseMod:

Mod={isExpr}∪{modx|x∈Identifier}Use={usex|x∈Identifier}

󰀂Use

UseMod={⊥,󰀘}∪i∈Mod2

TheUsesetisorderedbysupersetinclusion,andUseModisorderedasadisjointunion:For(i1,S1),(i2,S2)∈UseMod,(i1,S1)󰀝(i2,S2)iffi1=i2andS2⊆S1,andalso⊥󰀝vandv󰀝󰀘,forallv∈UseMod.(Intheexamples,wewillcontinuetowrite(modx,S)as{modx}∪Sand(isExpr,S)asS.)

Next,wecandefinepreciselyhowtomapasingleexpressionorassignmenttoitsUse-Modapproximation:

α0:Command∪Expression→UseMod

α0(x:=e)=(modx,{usev|vappearsine})α0(e)=(isExpr,{usev|vappearsine})

Wedefine󰀃theloweradjoint,α,ofaGaloisconnectionintheexpectedway:α(S)={α0(s)|s∈S}.Thematetoαmustbethisγ:

γ:UseMod→2

γ(isExpr,S)={e|v∈Simpliesv∈e}γ(modx,S)={x:=e|v∈Simpliesv∈e}γ(⊥)={},γ(󰀘)=Command∪Expression

Command∪Expression

p1,nil

{usex}p3,nil

{mody}

{usex}p2,nil

{usex,modx}

nil

ofanunfoldedPrologprogramiscontrolledbyjoiningtogethergoalclausesthatusethesamepredicatesymbol.APrologprogramisthereforeabstractedintoasyntaxofregularexpressions.Schmidt[42]usesasimilarregularexpressionlanguagetoabstractthesyntaxofpi-calculusconfigurations.Approximationsofprogramsyntaxbysetsofcontext-freegrammarruleshavebeendoneforfunctionalprogramsbyGiannottiandLatella[23]andforpi-calculusprogramsbyVenet[52,53].

AbstractActionsasAbstractOperations

Intheabovenarrative,wedidnotplaceformalrestrictionsontheformofGaloisconnectionthatrelatesconcreteactionstoabstractactions.Butinpractice,theconcreteactionsrepresentcommands—transferfunctions—thatupdateprogram

Ac

c2,withaconcretesemantics,andwhenstate.Whenwewriteatransition,c1−→Ac

a2,intheabstractsemantics,weassumewewritetheabstractedtransition,a1−→

thatthe“localsimulation”describedintheprevioussectionispreservedbytheabstractionofactions—c1safea1impliesc2safea2.Thispropertyissodesirable,wespendsometimetostudyit.

Consideraconcretedomain,Dcandtheabstractdomain,Da,connectedby

Store

aGaloisconnection(α,γ).(Standardinstantiationsofthesedomainsare2andAbsStoreoftheprevioussection,butastheabstractionprocessmaywellbeiterated,otherinstantiationsarepossibleaswell.)

TheGaloisconnectioninducesabinarysimulationrelation,safe⊆Dc×Daonthetwodomains(thatis,forallv∈Dc,u∈Da,vsafeuiffv󰀝γ(u),whereγ:Da→DcistheupperadjointoftheGaloisconnection).

Next,assumethateveryactionpossessesatransferfunction:Foreachaction,Ac∈Ac,let[[Ac]]c:Dc→Dcbeitstransferfunction,andsimilarly,foreachabstractedaction,Aa∈Aa,let[[Aa]]a:Da→Dabeitstransferfunction.(Thus,forthisstorytobesensible,abstractactionsmusthavetransferfunctionsaswell.)

Thedesiredpreservationpropertyforactionabstractionreadsasfollows:

forallAc∈Ac,andforallAa∈Aa,suchthatAaabstractsAc,

forallv∈Dc,u∈Da,vsafeuimplies[[Ac]]c(v)safe[[Aa]]a(u)(By“AaabstractsAc,”wemeanofcoursethatAc∈γA(Aa)orequivalently,αA(Ac)󰀝Aa,usingtheGaloisconnection,(αA,γC),betweenthetwoactionsets.)

IfonedecodestheconsequentoftheimplicationintotheGaloisconnectionbetweenDcandDa,oneobtainsthisinclusionattheconcretelevelDc:

󰀄

{[[Ac]]c(v)|v󰀝γ(u)}󰀝γ([[Aa]]a(u))whichisequivalenttothefollowinginclusiononthefunctionallevel,whichwewilluseinthenextsection:

α◦[[Ac]]c󰀝[[Aa]]a◦α

Fromhereon,wedemandthefollowingoftheabstractionofconcreteactionstoabstractactions:ifAaabstractsAc,thenα◦[[Ac]]c󰀝[[Aa]]a◦α.Thatis,theabstractionofactionspreservessimulationonprogramstates.

RemarkDependingontheabstractionofprogramstate,thepreservationprop-ertyjustdefinedcanbeachievedtrivially.Consideragainthelive-variablesexam-pleinFigure7,whereboththe“concrete”and“abstract”storesetsaremerely{nil}.(IntheFigure,wedonotcareaboutthevalueofstore,becauseitisthein-formationonthearcsoftheprogrammodelthatmatter.)Thesemantictransferfunctionsforboth“concrete”and“abstractactions”aretrivial.

Wecanmakethelive-variablesexamplemoreinterestingbylettingconcreteandabstractprogramstorestelluswhichexpressionswill-be-usedeforallexpres-sionse.Assignmentsoftheformx:=toperateontheseentitiesbackwardsinthefollowingfashion:

[[x:=t]]c(S)={e|eisasubexpressionoftor(e∈Sand[e]σ=[e]σ[[t]σ/x])}whereastheoperationofthecorrespondingUse-Modabstraction,whichweas-sumeheretobestraightforwardlyextendedtoexpressions,isdefinedby[[α0(x:=t)]]a(S)={e|usee∈α0(x:=t)or(e∈Sandmode∈α0(x:=t))}

Aslongaswedonotchangethegraphstructureoftheunderlyingprogrammodel,itiseasytoverifythattheUse-Modabstractioncomputesasafeapproximationoftheconcretewill-be-usedeinformationinthefollowingsense:Whenevertheabstractanalysistellsusthatanexpressionwillbeusedinfuturethenthisholdsalsooftheconcreteanalysis.(Thereareobviouslysituationswherethereverseimplicationfails.)

Thefollowingsectionaddressestheproblemofchanginggraphstructure,e.g.thecollapsingofnodes,whichisessentialforfightingthestateexplosionproblem.SimulationRelations

Theprevioussectionsformalizedinwhatsenseaconcretevalue/operation/actionissafelysimulatedorapproximatedbyanabstractvalue/operation/action;thesesimulationsare“local,”anditistimetoextendsimulationtoprogrammodels,givingusa“globalsimulation”propertythatholdsbetweenprogrammodels,sothatwecansaypreciselywhenaprogrammodelbuiltwithabstractoper-ationsandtransitionssafelydescribesaconcreteprogramexecution,whichisrepresentedbyaconcreteprogrammodel.Let,therefore

–Pc=(Sc,Ac,→c,sc,Ec)andPa=(Sa,Aa,→a,sa,Ea)betwoprogrammodels,

–DcandDabecompletelatticesconstitutingtheconcreterespectivelyab-stractdomains

–[[.]]c:Ac→(Dc→Dc)and[[.]]a:Aa→(Da→Da)meaningfunctions,associatingmonotone/distributivetransferfunctionswiththeirargumentac-tions,

–(α,γ)beapairofadjointsforDcandDa,

Underthesecircumstances,wewishtoformalizethatPcissafelyapproximatedbyPa.TheintuitionisthateveryexecutionpathinPcisimitatedbyoneinPa.Sincethearrowsinthepathsarelabelledwithactions,wemustalsoverifythatthecorrespondinglabelsonthecorrespondingarrowsarecompatibleaccordingtotheabstractionfunction.

Inthissetting,thenotionofsafeapproximationisessentiallythepropertyofsimulationfromconcurrencytheory.Weformalizetheseintuitionspreciselybymeansofasimulationrelation,Rα:

Paα-simulatesPc,iffthereexistsabinaryrelationRα∈Sc×Sasatisfyingthat

–(sc,sa)∈Rα

–foreachpair(s,t)∈Rα,andallAc∈Acthat:

AcAa󰀆󰀆s−→guaranteesatransitiont−→withcsat•(s󰀆,t󰀆)∈Rαand

•α◦[[Ac]]c󰀝[[Aa]]a◦α

Itshouldbenotedthattheunionofallsimulationrelations,󰀚α,isagainasimulationrelation.Indeed,thelargestpossiblesimulationsatisfyingtheaboverelationisexactlythisunionandisalsothegreatest-fixedpointofthefunctionaldefinedbytherecursivedefinition[1,16,36,35].ThusaprogrammodelPaglob-allysimulatesaprogrammodelPc,iff(sc,sa)∈󰀚α,whichwewillinfuturewritelikesc󰀚αsa.

Aspromisedintheprevioussection,weusethepreservationofprogramstateproperty,α◦[[Ac]]c󰀝[[Aa]]a◦α,toassertthatconcreteactions,Ac,aresafelyabstractedbyabstractactions,Aa.

Ouruseofsimulationtorelateprogrammodelsisacontinuationofthema-chineryusedintheearliersections:Recallthatasimulationrelation,safe,canbeusedinsafetyproofsifitisG-closed,andsafedefinesaGaloisconnectionifitisUG-closed.Althoughwedonotproveithere,anα-simulation,󰀚α,isU-closed,whenoneordersthesetofabstractprogrammodelssothatsa1󰀝sa2wheneverypathinsa1existsinsa2.Ifwerefinetheorderingtotakeintoaccountthepartialorderingsontheinformationonthenodesandarcs,wecanprovethat󰀚αisUG-closed.So,Galoisconnectionnotionscarryforwardtothetoplevelofourlevelsofabstraction.

GuaranteeingGlobalSafety

Asmentionedalready,theprimarynotionofcorrectness(safety)isbasedonatransformationalview:theinformationorpropertycomputedforacertainprogrampointmustbevalidwheneveraprogramexecutionreachesthispoint!Dataflowanalysesormodelcheckingtypicallyguaranteethiscriterionforafixedlevelofabstraction.α−simulationsprovideaframeworktoguaranteethis

correctnesscriterionforbackwardssafetypropertiesinthecontextofabstractioninthefollowingsense:11

sc󰀚αsaimpliessa|=aφ⇒sc|=cφforallbackwardssafetypropertiesΦ.Thus,undertheconsideredcircumstances,“globalsimulation”guarantees“localsimulation”.

Forforwardanalyseswehavetoconsiderbackwardssimulations12inordertoobtainasimilarresult.Luckily,manyabstractionsonprogrammodelscanbeusedforbothforwardsandbackwardsanalyses.Inthesecases,allsafetypropertiesoftheabstractmodelalsoholdoftheconcretemodel.GuaranteeingtheSimulationProperty

Twopreservationpropertiesareofinterest,oneconcerningtheoperationalse-manticsandoneconcerningprogrammodels.

AbstractionoftheOperationalSemantics.Onceonehasdefinedsimulations/Galoisconnectionsfortheconcreteandabstractdomainsandalsofortheconcreteandabstractactions,thenonecaninstantiatethesmall-stepsemanticsruleschemeswiththeconcretedomains/actionsandonecaninstantiatetheruleschemeswiththeabstractdomains/actions.Asacorollary,onewantstheresultthatthecon-cretesemanticsrulesare“simulated”bytheabstractsemanticsrules.Andinfact,in[43],thisresultisindeedprovedtrueforstate-transitionoperationalseman-tics.ButforthericherformatofStructuralOperationalSemantics,onerequiresapreciseformalizationofwhatitmeanstoinstantiatetheruleschemes,ataskgoingwellbeyondthescopeofthispaper.Thereaderisreferredto[3,16,45]fortherelevantmachinery.

Theseresultonlyaddress(forwardsimulation)andthereforeonlyguaranteethepreservationofbackwardsanalysisforsafety.

AbstractionoftheProgramModels.Besidesabstractiononthedomainandactionlevel,whichareadmissibleaslongascorrespondingGaloisconnectionsexist,thetypicaltransformationstepsarecollapsing,i.e.,identificationofnodesontheabstractlevelwhilecollectingthetransitionpotential,andunfolding,i.e.,copyingofsubgraphswithseveralentries.Whereascollapsingisclearlyanabstraction,unfoldinglookslikeaconcretizationatfirstsight,and,indeed,itisonlyanabstractionifitgoeshandinhandwithanabstractiononthedomainlevel,wheretheconcretedomainalsodistinguishesthedifferentversionsofduplicatednodes.Wehave:

–Locallycorrectabstractiononthedomainandactionside–characterizedbytheequationα◦[[Ac]]c󰀝[[Aa]]a◦α–togetherwithanykindofcollapsingguaranteestheexistenceofaforwardsandbackwardssimulation.Thusitsupportstheverificationofallsafetyproperties.

–Unfoldingpreservesforwardssimulationonly.Infact,itliesinthekernelofsimulation,i.e.argumentandresultmodelsimulateeachotherbothways.Thusunfoldingcanfreelybeusedwheneveronlybackwardsanalysisforsafetyisconcerned.

Theseareonlyafewsufficientconditionsforguaranteeingthepreservationofsimulation,andthereisahugepotentialforelaborationhereandforenlargingtheclassofpossiblesimulation-preservingconstructionsandtransformations.Thussimulationprovidesapowerfulbackgroundforestablishingsafetypreservingabstractions.

6CollectingSemantics

Onecanconstructanabstractinterpretationinordertoextractfromitacol-lectingsemantics.Acollectingsemanticsisinformationextractedfromthenodesandpathsofacomputationgraph.Theclassic,“first-order”[38]collectingse-manticsextractsthestatesfromacomputationgraph:Foraprogrammodel(oringeneral,agraph),g,itsfirst-ordercollectingsemanticshasformcollg:

Val

ProgramPoint→2andisdefined

collg(p)={v|(p,v)isanodeing}

Constant-propagationandtype-inferenceanalysescalculateanswersthatarefirst-ordercollectingsemantics.

Anotherformofcollectingsemanticsis“secondorder”orpathbased;itex-tractspathsfromthemodel.Thesetofpathsthatgointoaprogrampoint,p,isdefined

fcollg(p)={r|risapathingfromroot(g)tosome(p,v)}

andthesetofpathsthatemanatefrompis

bcollg(p)={r|risamaximalpathingsuchthatroot(r)=(p,v)}Thetwocollectingsemanticsarenamedfcollandbcollbecausetheyunderlietheinformationoneobtainsfromforwardsandbackwardsiterativeflowanalyses,re-spectively.Forexample,alive-variablesanalysiscalculates(propertiesof)bcollg,andanavailableexpressionsanalysiscalculates(propertiesof)fcollg.

Theaboveformsofcollectingsemanticsare“primitive”inthesensethatnojudgementabouttheextractedinformationismade.Inpractice,theinformationonedesiresfromadata-flowanalysisisajudgementwhethersomepropertyholdstrueoftheinputvaluestoaprogrampointorofthepathsflowinginto/outofaprogrampoint.(Forexample,alive-variablesanalysismakesjudgementsaboutwhichvariablesareliveforprogrampointpinpathsinbcollg(p).)

Toincludesuchjudgements,CousotandCousot[17]suggestthatamodel’scollectingsemanticscanbeasetofpropertiesexpressedinsomelogic,L.Givenaprogrammodel,g,andaproposition,φ∈L,wewriteφ∈[[g]]ifφholdstrueofg.

Forjudgementstobeuseful,werequireaweakconsistencypropertyof󰀚αandL:

gC󰀚αgA⇒(forallφ∈L,φ∈[[ga]]⇒φ∈[[gC]])

Thatis,anypropertypossessedbyanabstractmodel,gA,mustalsoholdforacorrespondingconcretemodel,gC.Bytighteningthetwoimplicationsintheaboveformulaintologicalequivalences,weobtainweakcompletenessandstrongcompleteness,respectively.Theformerisstudiedin[17];thelatterisemployedtojustifycorrectnessofreductionsofstatespacesinconcurrencytheory[9,18,32].

Withthisviewpoint,theextractionofcollectingsemantics—flowinformation—isinfacttheextractionofpropertiesfromaprogrammodel.Thissuggeststhatthereislittledifferencebetweenthecollectionofdata-flowinformationandthevalidationoflogicalsafetyandlivenesspropertiesfromaprogrammodel.Sincevalidationofpropertiesoffinite-statemodelscanbedonewithamodelchecker,modelcheckingbecomesthenaturaltoolforcomputingcollectingseman-tics,13wherecollectingsemanticsisencodedaslogicalproperties,assuggestedabove.Inthenextsection,weemployamodelcheckertocalculatecollectingsemanticsencodedaspropertiesinCTL.

7AnAnalysisMethodology

Theprevioussectionshaveintroducedthenecessarytechniquesforconstruction,abstraction,andanalysisofprogrammodels.Whenthetechniquesareorganizedintoamethodologyforprograminterpretationandstaticanalysis,thefollowingthreestageapproachtoabstractionappears,aframeworkthatwehaveusedinpractice:

ThreeStagesofAbstraction

sourceprogram+abstractionofinputdata

generateabstractcomputationgraph

finiteprogrammodel:

arcslabelledbyprogramactions,nodeslabelledbyabstractstates

replacelabelsbyabstractions

finiteprogrammodel:

arcslabelledbyabstractactions,nodeslabelledbyabstractstates

extractcollectingsemanticsby

checkingthemodelwithformulasinCTL

staticanalysisresults

abouttheinformationatitsstates(nodes)anditsactions(thelabelsonthearcsofitspaths),andonecollectsthisinformationintoastaticanalysis,whichisrightlyanabstractionoftheprogrammodelitself.QueryingandCollectingDataFlowInformation

AssuggestedbytheprevioussectionandSection3,thequeriesonemakesoftheprogrammodelcanbegiveninatemporallogicsuchasCTL,orbetterintheversionofCTLwiththeparameterizedHenceforthoperatorconsideredhere.14Forexample,onecanassembleacompletesummaryofdead-variableinformation15byaskingthefollowingquestion,foreachstate(node)ofaprogrammodelwhosearcsarelabelledwithUse-Modinformation

isDeadx=AG{a|a=usex}(¬end∧󰀟modx󰀗ff)

foreachvariable,x,inthesourceprogram.Theanswerstoallthesequeriesarecollectedtogether;theyconstituteadead-variablesanalysis.

CTLisagoodlanguageforstatingqueriesaboutaprogrammodel,becauseitisalanguageforexpressingpatternsofinformationthatoneencounterswhenonetraversesthepathsofamodel.Indeed,moststaticanalysesaredefinedtocollectinformationaboutthepatternsofstatesandactionsoneencountersalongaprogram’sexecutionpaths.

Forexample,dead-variablesanalysisisastaticanalysisthatcalculates,foreachprogrampoint,thepathsthatconnectaprogrampoint,p,tousesofvari-ables.(Ifavariable,x,isnotusedattheendofanysuchpathfromp,itis“dead”atp.)Whenabit-vector-baseddead-variablesanalysisdoesasimilarcalculation,itattachesabitvector,onebitperprogramvariable,toeachprogrampoint,p.Thebitforvariablexatpisset“off”ifthereexistsapathfromptoauseofx,whichmakesthevariablelive.Thus,thebitsinabit-vectorencodeasetofyes-noanswerstoqueriesaboutthestateofvariablesalongprogrampaths,andavariableisdeadatpifitsbitmaintainsitsinitialvaluetrue.

Asimilarstorycanbetoldforotherbit-vector-based,iterativedata-flowanalyses—thebitvectorsencodetheanswerstoqueriesaboutthepathslead-ingoutof(orthepathsleadinginto)theprogrampointsinaprogrammodel.Inthisway,bit-vectoranalysesareneatlydescribedbyourframework.Buttheframeworkcandomorethanhandlejustbit-vector-baseddata-flowanalyses.BeyondBitvectorAnalyses

1.Atthefirstabstractionstage,abstractionofstate,onecanusenontriv-ialabstractions—even-oddproperties,signproperties,finite-ranges-of-valuesproperties,constant-valueproperties—togenerateprogrammodelsmorepre-cisethanjustacontrol-flowgraph.The“precision”inthiscasemightmeanthattheprogrammodelissmallerthanthecontrol-flowgraph,whichmay

bethecasewhentheadditionalinformationsufficestoevaluateconditionals,orthattheprogrampointsare“split”(duplicatedwithdifferentstorevaluesatdifferentnodes),producingwhatthepartial-evaluationcommunitycallsapolyvariantanalysis[26].Thesameideaalsounderliestheproperty-orientedexpansionproposedin[49].

Inaddition,aprogram’sinputdatacanberestrictedtoreflectaprecondition.Forexample,thefirstprogrammodelinFigure6showstheprecisiononegainswhenoneknowsfromtheoutsetthatinputvariablexmustberestrictedtoanoddnumber.

2.Atthesecondabstractionstage,abstractionofactions,onecandoabstrac-tionofactionstootherformsofinformationbesidesUse-Modinformation.Astandardexampleofactionabstractionisseeninthebehaviourtreesgen-eratedbyCCS-expressions[35],whereactionsareabstractedto“channels.”Also,onemightabstractallactionstonil;whichwouldbeappropriateforcalculationsof“first-ordercollectingsemantics,”assuggestedinSection6.3.Atthethirdstage,theextractionofcollectingsemantics,onemightuseoneofavarietyoflogicstoaskquestionsoftheprogrammodel.AlternativestoCTL,suchasCTL*,LTL,mu-calculus,andB¨uchiautomata,canalsobeusedthisway,andthenextsectiongivesexamples.

Finally,onecanusetheprogramlogictovalidatesafetypropertiesaboutpathsintheprogrammodel.Thatis,theCTLformulaweusetoextractcollectingsemanticsisalsoalogicalpropositionstatinga“safetyproperty”ofapath.Andofcourse,programvalidationofrealsafetypropertiescanbeperformedintheverysameframeworkthatwehavepromotedfordata-flowanalysis.Ofcourse,thedualiswellknown:data-flowanalysishasbeenusedforprogramvalidation[19,33,34,39,40],butthepointhasnotbeenmadeasstronglyashere,whereweusetheverysamelogicforbothflowanalysisandprogramvalidation.Anotherbenefitfromtheframeworkpresentedhereistheclarificationitgivestothestagesofastaticanalysis—onecan,atleastconceptually,buildaprogrammodelfirstandextractstaticinformationfromitsecond.16Often,thesetwostagesareintertwinedinpresentationsofstaticanalyses,makingcorrectnessproofshardertowriteandextensionshardertoimplement.

8Discussion

Wenowdiscussseveralapplicationswhereourmethodologyledtoimprovedsolutionsofstaticanalysisproblems.StateExplosion

Considerpropertyvalidationforlargeprogramsorforsystemsofcommunicatingprocesses:Ifonegeneratesaprogrammodelforasystemofprocesses,themodel’s

statespacequicklybecomesintractable.Onesolutionistoconstructanaiveprogramgraphmodel,wheremany—perhaps,toomany—statesaremerged,andthepriceonepaysisthatthemergedstatesgeneratemanynewpathsthatareimpossibleinpractice.Suchimpossiblepathsthwartvalidationofelementarysafetyproperties.

State-spaceexplosionarisesinmodelconstructionforsinglesequentialpro-grams,aswell.Tolimitstatespace,acompilerbuildsanaiveprogrammodel—theprogram’scontrol-flowgraph—whichcontainsmanymorepathsthanwhatwillactuallybeusedduringexecution.Theextrapathsmightwellpreventvalidationofsafetyproperties.Hereisacontrivedexample:thecontrol-flowgraphfortheprogram,ifeven(x)thenx:=succxfi;ifodd(x)thenx:=0elsex:=1fi,containstwoimpossiblepaths,whichpreventvalidationthattheprogrammustterminatewithxequals0.IncrementalRefinement

Forthesereasons,onewantsamechanismthatincrementallyrefinesanaivepro-grammodel,eliminatingimpossiblepaths.Weillustratehereatechniquebasedonfilters[20].

SaythatwebeginwithanaiveprogrammodelandtrytovalidatethatΦholdstrueforallpathsinthemodel.Perhapsthevalidationfails,becausethenaivemodelincludesimpossiblepathsthatmakeΦfalse.Wewanttorefinethemodel—notabandonit—andrepeattheattemptatvalidation.Todoso,wedefineanadditionalabstractinterpretationandapplyittothenaiveprogrammodel.Wedosobyencodingtheabstractinterpretationasaproposition,Ψ,andwemodelchecktheformula,Ψ⇒Φ,oneverypathofthenaivemodel.Theabstractinterpretation,codedasΨ,filtersout,onthefly,impossiblepaths.Thistechniqueisreminiscentofastandardpracticeinmodelchecking,thatofattachinglogicalpreconditionstostrengthenthehypothesisofaformulatobeproved(forexample,limitingmodelsearchtojustfairpaths,e.g.,isFairPath⇒Φ[7,8]).Butwhatisnotablehereisthatanabstractinterpretation,ratherthanalogicalprecondition,isattached.ThistechniquehasbeenusedwithsuccessbyDwyerandPasareanu[21]onavarietyofproblemsincommunicatingsystems.AnabstractinterpretationthatusesafinitedomainofabstractvaluescanbeencodedasapathpropositioninthisvariantofLTL:

Ψ::=β|X|Ψ∧Ψ|¬Ψ|󰀟A󰀗Ψ|νX.Ψ

RecallthatLTLislogicofpaths:forapath,p,saythatp|=βifstateformulaβ

A

holdstrueforp’sstartstate;p|=󰀟A󰀗Ψholdsifp=s0−→p1,andp1|=Ψholds(thisisthe“nextstate”modality);andp|=νX.Ψholdsiffp|=[νX.Ψ/X]Ψ,thatis,νX.Ψisarecursiveproposition.CharacterizingAutomata

TounderstandhowtouseLTL,weexploitthecorrespondencebetweenfinite-stateautomataandLTL,andpresentinFigure8anautomatonthatencodeseven-oddabstractinterpretationofavariable,x.

Fig.8.Even-oddabstractinterpretationencodedasapathformula

Itiseasytoimaginethisautomatonexecutedonthepathsofacontrol-flowgraph—aslongastheautomatoncancontinuetomovewhileittraversesapath,thepathiswell-formedwithrespecttotheeven-odd-nessvalueofx.17Theautomaton“filtersout”thosepathsinanaivemodelthatareimpossiblewithrespecttox’seven-odd-ness,andintheprocessgeneratesamoreaccurate,restricted,reducedmodel.(Considertheexampleprogramatthebeginningofthissection—theimpossiblepathsarefilteredout.)

Next,imaginetheautomatonexecutedonthenaivemodelinparallelwithamodelcheckofasafetyproperty,Φ.ThiswouldvalidateΦjustonthosepathswellformedwithrespecttox’seven-odd-ness.Nointermediate,reducedmodelisbuilt;theworkisdoneonthenaivemodel.

TheautomatonintheFigureisjustapictorialrepresentationofthisLTLformula:(Forbrevity,welimitthesetofactionstojustevenx,¬evenx,x:=x+1,andy:=2.)

isEvenxiff󰀟evenx󰀗isEvenx

󰀟x:=x+1󰀗isOddx󰀟y:=2󰀗isEvenxisFinalState

isOddxiff󰀟¬evenx󰀗isOddx

󰀟x:=x+1󰀗isEvenx󰀟y:=2󰀗isOddxisFinalState

Thus,theparallelexecutionofeven-oddanalysiswiththemodelcheckingofsafetypropertyΦisjustthemodelcheckoftheformula

(isEvenx⇒Φ)∧(isOddx⇒Φ)

BindingTimeinProgramAnalysis

Themethodproposedaboveisbasedontheobservationthatprogramanalysiscanberefinedbyverifyingimplicationsonthelogicallevel,whichrestrictstheconditionsunderwhichacertainpropertymusthold,or,equivalently,byverifyingtheoriginalpropertyforaproductprogrammodelconsistingoftheoriginalprogrammodelanda‘filter’automatonwhichrestrictsthebehaviouroftheprogrammodeltoitsdesiredfragment.Thisispossible,becausetheformulaeconsideredaspremisescanbefullyexpressedintermsofautomata.Basedonthisidea,itisnowpossibletochoose

–wheretoputthecomplexity:intheformulaorintheautomaton,–howtocombinetheproductconstructionandthemodelchecking.

Straightforwardwouldbetofirstcomputetheproductprogrammodelandsub-sequentlyapplythemodelchecker,assuggestedintheprevioussection.Thiswoulddirectlycorrespondstotheproperty-orientedexpansionapproachpro-posedin[49],whichconsidersproductconstructionwithautomataspecifiedindifferentparadigmsaccordingtotheunifyingmodelideapresentedin[50].

However,asalsomentionedintheprevioussection,thereare‘on-the-fly’modelcheckersallowingtoconstructtheproductprogrammodelondemandduringthemodelcheckingprocedure,whichmayhelptoavoidthestateexplo-sionproblem.Infact,thesamemethodcanalsobeappliedifonewantstoverifyaparallelprogram.

Inthisway,thelinebetweenabstractinterpretationinmodelconstructionandpropertyextractionviamodelcheckinghasbeenblurred.Theissuebecomesoneof“bindingtimes”—whenistheabstractinterpretation“bound”intotheprogrammodel?Theansweroftenhingesonthedesiredcomplexityofthemodelversusthecomplexityoftheformulatobemodelchecked.

9Conclusion

Thispaperhasattemptedtoexplainhowabstractinterpretation,flowanalysis,andmodelcheckingcaninteractwithinacomprehensivestaticanalysismethod-ology.Inparticular,wehopedtoemphasizethatthemachineryandmethodsofflowanalysis,abstractinterpretation,andmodelcheckinghavegrowntogether,andthatresearcherscanprofitablyusetechniquesfromoneareatoimproveresultsintheothers.

Inthefuture,itisplannedtospecificallysupportthestudyofmethodinterac-tion,inordertoimprovetheunderstandingoftheinterdependenciesbetweenandthe‘optimal’problem-specificcombinationsofalgorithmsfore.g.modelconstruc-tion,abstractionandanalysisasaddressedhere.Acorrespondingpublicplatformisalreadyavailable[46],anditisgoingtobeusedinprogramanalysis[51].

Acknowledgements

WearegratefultoTizianaMargariaforproofreading,toMarkusM¨uller-Olmforhisconstructivecriticism,andtoAndreasHolzmannforhissupportinthetypesetting.

References

1.P.Aczel.Non-Well-FoundedSets,LectureNotes14,CenterforStudyofLanguageandInformation,Stanford,CA,1988.

2.S.BensalemandA.BouajjaniandC.LoiseauxandJ.Sifakis.Propertypreservingsimulations.ComputerAidedVerification:CAV’92.LectureNotesinComputerScience663,Springer,1992,260–273.

3.D.Berry.GeneratingProgramAnimatorsfromProgrammingLanguageSemantics,Ph.D.Thesis,LFCSReportECS-LFCS-91-148,UniversityofEdinburgh,1991.4.O.BurkartandB.Steffen.ModelCheckingforContext-FreeProcesses.ProceedingsoftheInternationalConferenceonConcurrencyTheory,Concur95,LNCS630,19925.S.C.CheungandJ.Kramer.AnIntegratedMethodForEffectiveBehaviourAnal-ysisofDistributedSystems.Proceedingsofthe16thInternationalConferenceonSoftwareEngineering,Sorrento,CA,USA,1994,pp.309–320.

6.S.C.CheungandJ.Kramer.TractableFlowAnalysisforDistributedSystems.IEEETransactionsonSoftwareEngineering20-9(1994).

7.E.ClarkeandE.EmersonandA.Sistla.Automaticverificationoffinite-statecon-currentsystemsusingtemporallogicspecifications.ACMTransactionsonProgram-mingLanguagesandSystems8(1986)244–263.

8.E.M.ClarkeandO.GrumbergandD.E.Long.Verificationtoolsforfinite-stateconcurrentsystems.InADecadeofConcurrency:ReflectionsandPerspectives,J.W.deBakkerandW.-P.deRoeverandG.Rozenberg”,editors,SpringerLNCS803,1993,pp.124-175.

9.R.CleavelandandP.IyerandD.Yankelevich.Optimalityinabstractionsofmodelchecking.Proc.SAS’95:Proc.2d.StaticAnalysisSymposium,LectureNotesinComputerScience983,Springer,1995,1995.

10.R.Cleaveland,M.KleinandB.Steffen.FasterModelCheckingfortheModalµ-Calculus.ProceedingsoftheInternationalWorkshoponComputerAidedVerifica-tion,CAV’92,LNCS663,1992

11.M.CodishandS.DebrayandR.Giacobazzi.Compositionalanalysisofmodular

logicprograms.Proc.20thACMSymp.onPrinciplesofProgrammingLanguages,1993,pp.451-4.

12.M.CodishandM.FalaschiandK.Marriott,Suspensionanalysisforconcurrent

logicprograms.Proc.8thInt’l.Conf.onLogicProgramming,MITPress,1991,pp.331-345.

13.G.CousineauandM.Nivat.Onrationalexpressionsrepresentinginfiniterational

trees.Proc.8thConf.Math.FoundationsofComputerScience:MFCS’79,LectureNotesinComputerScience74,Springer,1979,pp.567–580.

14.P.Cousot,R.Cousot.Abstractinterpretation:AunifiedLatticeModelforstatic

AnalysisofProgramsbyConstructionorApproximationofFixpoints.InProceed-ings4thACMSymp.onPrinciplesofProgrammingLanguages,POPL’77,LosAngeles,California,January,1977

15.P.CousotandR.Cousot.Systematicdesignofprogramanalysisframeworks.Proc.

6thACMSymp.onPrinciplesofProgrammingLanguages,POPL’79,1979,pages269-282.

16.P.CousotandR.Cousot.InductiveDefinitions,Semantics,andAbstractInterpre-tation.Proc.19thACMSymp.onPrinciplesofProgrammingLanguages,POPL’92,1992,pp.83–94.

17.P.CousotandR.Cousot.Abstractinterpretationframeworks.JournalofLogicand

Computation2(1992)511-7.

18.D.Dams.Abstractinterpretationandpartitionrefinementformodelchecking.Ph.D.

thesis,TechnischeUniversiteitEindhoven,TheNetherlands,1996.

19.M.DwyerandL.Clark.DataFlowAnalysisforVerifyingPropertiesofConcur-rentPrograms.Proc.2dACMSIGSOFTSymposiumonFoundationsofSoftwareEngineering,1994,pp.62-75.

20.M.DwyerandD.Schmidt,LimitingStateExplosionwithFilter-Based

Refinement.Proc.InternationalWorkshoponVerification,ModelCheck-ingandAbstractInterpretation,PortJefferson,LongIsland,N.Y.,http://www.cis.ksu.edu/~schmidt/papers/filter.ps.Z,1997.

21.M.DwyerandC.Pasareanu.Filter-basedModelCheckingofPartialSystems.Pro-ceedingsofthe6thACMSIGSOFTSymposiumontheFoundationsofSoftwareEngineering,Orlando,FL,USA,1998.

22.E.Emerson,J.Lei,Efficientmodelcheckinginfragmentsofthepropositionalmu-calculus.InProceedingsLICS’86,267-278,1986

23.F.GiannottiandD.Latella,GatesplittinginLOTOSspecificationsusingabstract

interpretation.InProc.TAPSOFT’93,M.-C.GaudelandJ.-P.Jouannaud,eds.LNCS668,Springer,1993,pp.437-452.

24.Godefroid,P.andWolper,P.UsingPartialordersfortheefficientverificationof

deadlockfreedomandsafetyproperties.Proc.oftheThirdWorkshoponComputerAidedVerification,Springer-Verlag,LNCS575,1991,pp.417–428.25.M.Hecht,FlowAnalysisofComputerPrograms.Elsevier,1977

26.N.D.JonesandC.GomardandP.Sestoft,PartialEvaluationandAutomaticPro-gramGeneration.PrenticeHall,1993.

27.J.KamandJ.Ullman.Globaldataflowanalysisanditerativealgorithms.J.ournal

oftheACM23(1976)158–171.

28.G.A.Kildall.Aunifiedapproachtoglobalprogramoptimization.InConf.

Rec.1stACMSymposiumonPrinciplesofProgrammingLanguages(POPL’73),pages194–206.ACM,NewYork,1973.

29.J.Knoop,B.SteffenandJ.VollmerParallelismforFree:BitvectorAnalysis⇒

NoStateexplosion!ProceedingsoftheInternationalWorkshoponToolsandAl-gorithmsfortheConstructionandAnalysisofSystems,TACAS’95,LNCS1019,1995

30.J.Knoop,O.R¨uthingandB.Steffen.LazyCodeMotion.ProceedingsoftheACM

SIGPLAN’94ConferenceonProgrammingLanguageDesignandImplementation(PLDI’94),Olando,Florida,SIPLANNotices30,6(1994),233-245.

31.D.Kozen,Resultsonthepropositionalmu-calculus.TheoreticalComputerScience,

27(1983)333–3.

32.Y.S.Kwong,Onreductionofasynchronoussystems.TheoreticalComputerScience

5(1977)25–50.

33.S.P.MasticolaandB.G.Ryder.StaticInfiniteWaitAnomalyDetectioninPolyno-mialTime.ProceedingsofACMInternationalConferenceonParallelProcessing,1990.

34.S.P.MasticolaandB.G.Ryder.AModelofAdaProgramsforStaticDeadlockDetec-tioninPolynomialTime.ProceedingsACMWorkshoponParallelandDistributedDebugging,1991.

35.R.Milner.CommunicationandConcurrency.PrenticeHall,19.

36.R.MilnerandM.Tofte.Co-inductioninrelationalsemantics.TheoreticalCom-puterScience,17(1992)209-220.

37.A.MycroftandN.D.Jones.Arelationalframeworkforabstractinterpretation.In

ProgramsasDataObjects,LectureNotesinComputerScience217,Springer,1985,pp.156–171.

38.F.Nielson,ADenotationalFrameworkforDataFlowAnalysis.ActaInformatica

18(1982)265-287.

39.K.M.OlenderandL.J.Osterweil.Cecil:ASequencingConstraintLanguagefor

AutomaticStaticAnalysisGeneration.IEEETransactionsonSoftwareEngineering16-3(1990)268–280.

40.K.M.OlenderandL.J.Osterweil.InterproceduralStaticAnalysisofSequencing

Constraints.ACMTransactionsonSoftwareEngineeringandMethodology1-1(1992)21–52.

41.GordonD.Plotkin.AStructuralApproachtoOperationalSemantics.Technical

ReportDAIMIFN-19,UniversityofAarhus,Denmark,1981.

42.D.A.Schmidt,Abstractinterpretationofsmall-stepsemantics.Proc.5thLOMAPS

WorkshoponAnalysisandVerificationofMultiple-AgentLanguages,M.DamandF.Orava,eds.Springer,1996.

43.D.A.Schmidt,Trace-basedabstractinterpretationofoperationalsemantics.J.Lisp

andSymbolicComputation,10(1998)237-271.

44.D.A.Schmidt,Data-flowanalysisismodelcheckingofabstractinterpretations.

Proc.25thACMSymp.onPrinciplesofProg.Languages,POPL98,1998.

45.F.daSilva.CorrectnessProofsofCompilersandDebuggers:anApproachBasedon

StructuralOperationalSemantics.Ph.D.thesis,LFCSreportECS-LFCS-92-241,EdinburghUniversity,Scotland,1992.

46.B.Steffen,T.Margaria,V.Braun:TheElectronicToolIntegrationplatform:con-ceptsanddesign,[51]1(1),pp.9-30.

47.B.Steffen.DataFlowAnalysisasModelChecking.ProceedingsoftheInternational

ConcerenceonTheoreticalAspectsofComputerSoftware,TACS’91,LNCS526,1991

48.B.Steffen.GeneratingDataFlowAnalysisAlgorithmsfromModalSpecifications,

InternationalJournalonScienceofComputerProgramming,N.21,1993,pp.115-139.

49.B.Steffen,Property-orientedexpansion.Proc.StaticAnalysisSymposium:SAS’96,

LectureNotesinComputerScience1145.Springer,1996,pp.22–41.

50.B.Steffen,UnifyingModels.Proc.oftheAnnualSymposiumonTheoreticalAspects

ofComputerScience,STACS’97,LectureNotesinComputerScience1200.Springer,1997,pp.1–20.

51.SpecialSectiononProgrammingLanguageTools,Int.JournalonSoftwareToolsfor

TechnologyTransfer,Vol.3,SpringerVerlag,October1998

52.A.Venet,Abstractinterpretationofthepi-calculus.Proc.LOMAPSWorkshopon

AnalysisandVerificationofMultiple-AgentLanguages,M.DamandF.Orava,eds.,LNCS1192,Springer,1996.

53.A.Venet,AutomaticDeterminationofCommunicationTopologiesinMobileSys-tems.Proc.SAS’98,G.Levi,ed.SpringerLNCS,1998.