News
Currently, no news are available
Program Analysis
Course Organization
The course consists of two parts:
- Lectures and tutorials conducted in a block fashion from October 4 to October 20, i.e., before the start of the regular lecture period.
- Group projects carried out from early November to end of January.
The block lecture in October consists of two time slots per day, from 10:00 to 12:00 and from 14:00 to 16:00. The lectures will be held in room 024 (MPI-INF), except for the very first lecture on October 4 and the first lecture on October 18, which will take place in Hörsaal 1 (E1 3). The detailed schedule can be found here.
The first lecture takes place on October 4 at 10:00 in Hörsaal 1 (E1 3).
Introduction
Program analysis deals with automatic analysis of programs with regards to certain properties. Depending on the application, these properties could be related to safety, security, or correctness of the program. The analysis results are used for different purposes by different applications. Some such uses are:
- proving the absence of runtime errors, as is e.g. done by Astree
- statically analyzing the worst-case execution time (WCET) of the program
- checking for hardware side-channel vulnerabities such as Spectre
- guiding program transformations in compilers, e.g. for high performance computing
This course provides an overview of the different techniques used in the field, the concepts guiding them, and their applications. Topics covered in the course include but are not limited to:
- Basics on Fixed Point Theory
- Hoare Logic and Predicate Transformer Semantics
- Abstract Interpretation
- Data-flow Analysis and Interprocedural Analysis
- SMT solvers, Symbolic Execution, and Symbolic Abstraction
- Information Flow Analysis and Side-channel Analysis
- Quantitative Program Analysis (e.g. expected execution times of probabilistic programs)
Prerequisites
This course is open to advanced bachelor's students as well as to master's students.
While there are no specific course prerequisites for this advanced course, a solid background in discrete mathematics is highly recommended, as provided by undergraduate math courses in our bachelor's program. In addition, some programming experience would be valuable for the projects.