Generating program analyzers [Elektronische Ressource] / von Florian Martin

Generating Program AnalyzersDissertationZur Erlangung des Grades einesDoktors der Ingenieurwissenschaften (Dr.-Ing.)der Technischen Fakultat¨¨der Universitat des SaarlandesvonDiplom-InformatikerFlorian MartinSaarbr¨uckenJuni 1999Tag des Kolloquiums: 22.10.1999Dekan: Prof. Dr. W.J. PaulGutachter: Prof. Dr. R. WilhelmProf. H.R. Nielson, Ph.D.Vorsitzender: Prof. Dr.-Ing. G. WeikumiAbstractIn this work the automatic generation of program analyzers fromconcise specifications is presented. It focuses on provably correctand complex interprocedural analyses for real world sized imper-ative programs. Thus, a powerful and flexible specification mech-anism is required, enabling both correctness proofs and efficientimplementations. The generation process relies on the theory ofdata flow analysis and on abstract interpretation. The ofdata flow provides methods to efficiently implement anal-yses. Abstract interpretation provides the relation to the semanticsof the programming language. This allows the systematic deriva-tion of efficient provably correct, and terminating analyses. Theapproach has been implemented in the program analyzer genera-tor PAG. It addresses analyses ranging from “simple” intrapro-cedural bit vector frameworks to complex interprocedural aliasanalyses. A high level specialized functional language is used asspecification mechanism enabling elegant and concise specifica-tions even for complex analyses.