UndecidabilityofStaticAnalysis
`WilliamLandi
`SiemensCorporateResearchInc
`CollegeRdEast
`Princeton,NJ
`wlandi@scr.siemens.com
`Abstract
`StaticAnalysisofprogramsisindispensabletoanysoftwaretool,environment,orsystem
`thatrequirescompiletimeinformationaboutthesemanticsofprograms.Withthe
`emergenceoflanguageslikeCandLISP,StaticAnalysisofprogramswithdynamic
`storageandrecursivedatastructureshasbecomea(cid:12)eldofactiveresearch.Suchanalysis
`isdi(cid:14)cult,andtheStaticAnalysiscommunityhasrecognizedtheneedforsimplifying
`assumptionsandapproximatesolutions.However,evenunderthecommonsimplifying
`assumptions,suchanalysesareharderthanpreviouslyrecognized.Twofundamental
`StaticAnalysisproblemsareMayAliasandMustAlias.Theformerisnotrecursive
`(i.e.,isundecidable)andthelatterisnotrecursivelyenumerable(i.e.,isuncomputable),
`evenwhenallpathsareexecutableintheprogrambeinganalyzedforlanguageswith
`if-statements,loops,dynamicstorage,andrecursivedatastructures.
`CategoriesandSubjectDescriptors:D. . [ProgrammingLanguages]:Processors;F. . [Com-
`putationbyAbstractDevices]:ModelsofComputation(cid:0)bounded-actiondevices;F.. [Math
`LogicandFormalLanguages]:MathematicalLogic(cid:0)computabilitytheory
`GeneralTerms:Languages,Theory
`AdditionalKeyWordsandPhrases:Aliasanalysis,data(cid:13)owanalysis,abstractinterpretation,
`haltingproblem
`FromacmLettersonProgrammingLanguagesandSystems,
`Vol. ,No.,December ,Pages - .
`Permissiontocopywithoutfeeallorpartofthismaterialisgranted
`providedthatthecopiesarenotmadeordistributedfordirectcommercial
`advantage,theACMcopyrightnoticeandthetitleofthepublicationand
`itsdateappear,andnoticeisgiventhatcopyingisbypermissionofthe
`AssociationforComputingMachinery.Tocopyotherwise,ortorepublish,
`requiresafreeand/orspeci(cid:12)cpermission.
`c(cid:13) ACM - / / - $ .
`
`
`Columbia Ex 2038-1
`Symantec v Columbia
`IPR2015-00375
`
`
`WilliamLandi
`SiemensCorporateResearchInc
`CollegeRdEast
`Princeton,NJ
`wlandi@scr.siemens.com
`Abstract
`StaticAnalysisofprogramsisindispensabletoanysoftwaretool,environment,orsystem
`thatrequirescompiletimeinformationaboutthesemanticsofprograms.Withthe
`emergenceoflanguageslikeCandLISP,StaticAnalysisofprogramswithdynamic
`storageandrecursivedatastructureshasbecomea(cid:12)eldofactiveresearch.Suchanalysis
`isdi(cid:14)cult,andtheStaticAnalysiscommunityhasrecognizedtheneedforsimplifying
`assumptionsandapproximatesolutions.However,evenunderthecommonsimplifying
`assumptions,suchanalysesareharderthanpreviouslyrecognized.Twofundamental
`StaticAnalysisproblemsareMayAliasandMustAlias.Theformerisnotrecursive
`(i.e.,isundecidable)andthelatterisnotrecursivelyenumerable(i.e.,isuncomputable),
`evenwhenallpathsareexecutableintheprogrambeinganalyzedforlanguageswith
`if-statements,loops,dynamicstorage,andrecursivedatastructures.
`CategoriesandSubjectDescriptors:D. . [ProgrammingLanguages]:Processors;F. . [Com-
`putationbyAbstractDevices]:ModelsofComputation(cid:0)bounded-actiondevices;F.. [Math
`LogicandFormalLanguages]:MathematicalLogic(cid:0)computabilitytheory
`GeneralTerms:Languages,Theory
`AdditionalKeyWordsandPhrases:Aliasanalysis,data(cid:13)owanalysis,abstractinterpretation,
`haltingproblem
`FromacmLettersonProgrammingLanguagesandSystems,
`Vol. ,No.,December ,Pages - .
`Permissiontocopywithoutfeeallorpartofthismaterialisgranted
`providedthatthecopiesarenotmadeordistributedfordirectcommercial
`advantage,theACMcopyrightnoticeandthetitleofthepublicationand
`itsdateappear,andnoticeisgiventhatcopyingisbypermissionofthe
`AssociationforComputingMachinery.Tocopyotherwise,ortorepublish,
`requiresafreeand/orspeci(cid:12)cpermission.
`c(cid:13) ACM - / / - $ .
`
`
`Columbia Ex 2038-1
`Symantec v Columbia
`IPR2015-00375
`
`
`
`Introduction
`
`StaticAnalysisistheprocessesofextractingsemanticinformationaboutaprogramatcompile
`time.Oneclassicalexampleisthelivevariables[]problem;avariablexisliveatastatement
`si(cid:11)onsomeexecutionxisused(accessed)aftersisexecutedwithoutbeingrede(cid:12)ned.Other
`classicalproblemsincludereachingde(cid:12)nitions,availableexpressions,andverybusyexpressions[].
`TherearetwomainframeworksfordoingStaticAnalysis:DataFlowAnalysis[]andAbstract
`Interpretation[ ].Theframeworkisnotrelevanttothispaper,asweshowthattwofundamental
`StaticAnalysisproblemsareharderthanpreviouslyacknowledged,regardlessoftheframework
`used.WeviewthesolutiontoaStaticAnalysisproblemasthesetof\facts"thatholdforagiven
`program.Thus,forlivevariablesthesolutionisf(x;s)jvariablexisliveatstatementsg.With
`thatinmind,wereviewafewde(cid:12)nitions:
`(cid:15)Asetisrecursivei(cid:11)itcanbeacceptedbyaTuringmachinethathaltsonallinputs.
`(cid:15)Asetisrecursivelyenumerablei(cid:11)itcanbeacceptedbyaTuringmachinewhichmayormay
`nothaltonallinputs.
`StaticAnalysisoriginallyconcentratedonFORTRAN,andwaspredominatelycon(cid:12)nedtoa
`singleprocedure(intraproceduralanalysis)[, , ].However,eventhissimpleformofStatic
`Analysisisnotrecursive.Thedi(cid:14)cultyliesinconditionals.Thereare,ingeneral,manypaths
`throughaprocedure,butnotallpathscorrespondtoanexecution.Forexample,consider
`if(x>- )y= ;
`if(x<