F. Model checking software at compile time(7)

f={(l,Succ(l))|l∈Lf,Succ(l)={l‘|(l,l‘)∈Ef}}.Thismeans,theCFGtransitionrelationistrans-latedintoatransitionrelation,wherethetargetforeachtransitionisthesetoflocationswepossiblycanbranchto.ThisisaccordingtoNuSMV’ssyntaxanddoesnotchangetheoriginalCFGtransitionrelation.

Deff={de ne(p)={l|µf(l)=p,l∈Lf}|p∈Σf}.Whereeveryde ne(p)isaDEFINEdeclarationofpinNuSMV.Ade nedeclarationisaspaceef cientwaytodeclare,e.g.,thatapropositionalvariablepholdsexactlyinaparticularsetoflocations.Inourcase,that

4

3.4Architecture

ThearchitectureofourapproachisoutlinedinFigure1.GivenaC/C++program,theonlyinteractionneededfromtheuseristo

1.provideaCTLspeci cation,and

2.de netheatomicpropositionofthespeci cationintermsofqueriesasdescribedinSection3.2.ThetranslationofaprogramintotheCFG,thepat-ternmatching,thesubsequentlabeling,thetranslationtoNuSMV,aswellastheerrorreporting,areallfullyauto-matic.Thisreducestheburdenontheusertoaminimumandforgenericpre-de nedpropertiestozero.

4Example

Thissectionpresentsanexampletoillustratethepro-posedapproachofcombiningsyntacticcheckingwith