F. Model checking software at compile time(17)

[17]G.Holzmann.Staticsourcecodecheckingforuser-de ned

properties.Pasadena,CA,USA,June2002.

[18]K.RustanM.Leino,JamesB.SaxeandR.Stata.Checking

Javaprogramsviaguardedcommands.TechnicalReport1999-002,PaloAlto,CA,1999.[19]Klocwork.K7.

/products/klocworkk7.asp.[20]Microsoft.Prefast.

/whdc/devtools/tools/PREfast.mspx.[21]S.Muchnick.AdvancedCompilerDesignandImplementa-tion.MorganKaufmannPublishers,1997.[22]J.M¨uhlbergandG.L¨uttgen.BLASTingLinuxcode.In

Proc.ofthe11thInternationalWorkshoponFormalMeth-odsforIndustrialCriticalSystems(FMICS06),volume4346ofLNCS,Toappear.

[23]F.Nielson,H.R.Nielson,andC.L.Hankin.Principlesof

ProgramAnalysis.Springer,1999.[24]PolySpace.PolySpaceforC++.

/cpp.htm.

[25]J.-P.QueilleandJ.Sifakis.Speci cationandveri ca-tionofconcurrentsystemsinCESAR.InM.Dezani-CiancagliniandU.Montanari,editors,Proc.Intl.Sympo-siumonProgramming,Turin,April6–8,1982,pages337–350.Springer-Verlag,1982.

[26]B.SchlichandS.Kowalewski.ModelcheckingCsource

codeforembeddedsystems.InProc.oftheIEEE/NASAWorkshoponLeveragingApplicationsofFormalMethods,Veri cation,andValidation.NASA/CP-2005-212788,Sept2005.

[27]D.A.Schmidt.Data owanalysisismodelcheckingof

abstractinterpretations.InACMSIGPLAN-SIGACTSympo-siumonPrinciplesofProgrammingLanguages(POPL’98),NewYork,NY,USA,1998.ACMPress.

[28]D.A.SchmidtandB.Steffen.Programanalysisasmodel

checkingofabstractinterpretations.InIntl.SymposiumonStaticAnalysis(SAS’98),pages351–380,London,UK,1998.Springer-Verlag.

10