Short Course on Program Analysis

Reinhard Wilhelm, Saarland University, Alemania

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.
After a long development of program analysis methods and the identification of new applications, the underling theory was developed in the 1970s. This theory related program analysis to the semantics of the programming language. It provided the basis for correctness proofs and even for program analyses that were correct by construction.
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.

El curso será dictado en inglés. Para tomar este curso es necesario contar con conocimientos elementales de teoría de lenguajes o construcción de compiladores. La evaluación consiste en un examen, que se tomará el Sábado 27/7 por la mañana.

 

Materiales del curso

 

Acerca del profesor

Dr. Reinhard Wilhelm studied Mathematics, Physics, and Mathematical Logic at Westfälische Wilhelms-Universität Münster, Informatics at Technical University München and Stanford University. He holds a PhD from TU München. Since 1978 he is Full Professor of Informatics at Saarland University in Saarbrücken, and since 1990 he is the Scientific Director of the Leibniz Institute for Informatics in Schloss Dagstuhl. His research areas include programming languages and compiler construction, static program analysis, and embedded real-time systems. He is an ACM Fellow and has received the European IST Prize with AbsInt (2004), the Alwin Walther Medal (2006), the Prix Gay-Lussac-Humboldt (2007), the Konrad-Zuse Medal (200), the Federal Cross of Merit (Bundesverdienstkreuz am Band) (2010), and the ACM Distinguished Service Award (2010). He has been awarded honorary doctorates by RWTH Aachen and Tartu University.