Abstract: Static program analysis is a method to answer questions about properties of programs. As this method was developed to enable compilers to improve the efficiency of programs, traditional questions are: "Does program variable x always have the same value at program point p?", "Is the computation of expression e at program point p redundant?", and "Is program variable x live at program point p?". Given appropriate answers to these questions, the compiler would apply transformations that improve the efficiency of the program without changing the semantics of the program. For example, if the answer to the first question would be: "Yes, x always has value 5 at program point p.", the compiler would substitute 5 for x at p. The answers given by program analysis had always to be correct. Otherwise the compiler would change the semantics of the program.
Later program analysis became an automatic method for program verification. It is now used to prove that certain runtime errors, such as index-out-of-bounds, division by zero, or arithmetic overflows, do not occur. One particular application is the derivation of execution-time bounds for real-time programs.
This short course introduces several program analyses used in compilers and in program verification, based on an introduction of the foundations of program analysis.
Professor Reinhard Wilhelm: Professor of Informatics at Saarland University in Saarbrücken, and Scientific Director of the Leibniz Centre for Computer Science, Schloss Dagstuhl. His research activities have concentrated on the following areas: compiler design and generation, static program analysis, design and implementation of program analyses for the determination of worst-case execution times incorporating cache and pipeline behavior predictions, design of powerful shape analyses which determine the data structures a program is manipulating, techniques to generate visualizations and animations.