184.703 Program Analysis
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2022W, VU, 2.0h, 3.0EC


  • Semester hours: 2.0
  • Credits: 3.0
  • Type: VU Lecture and Exercise
  • Format: Online

Learning outcomes

After successful completion of the course, students are able to...

- apply static code analysis (for compiler construction and program verification),
- create new static analyses,
- prove the correctness of a static analysis,
- read and present current research literature on program analysis.

Subject of course

The lecture introduces into automated program analysis (this course mainly covers static code analysis). Static analysis has traditionally been been applied in compiler construction for optimizing the generated code. Modern development environments such as Visual Studio (invoke using /analyze flag when compiling) and the Clang project (Clang Static Analyzer) use static analysis for finding potential bugs already at compile time. This approach has been successfully been integrated into the development process of facebook (https://fbinfer.com/). Further, static analysis is a successful methodology for the verification of programs in safety-critical applications, for example for demonstrating that flight control software is free of runtime errors (https://www.absint.com/astree/index.htm).

In the lecture, we present
- simple static analyses, that are used routinely in compilers, such as Reaching Definitions, Live Variable Analysis and Constant Propagation, and more complex analyses, such as Pointer Analysis and Call Graph Analysis,
- static analyses for the generation of numeric invariants, which can be applied for program verification, such as Interval-, Octagon-, and Polyhedra analysis, as well as techniques for the generation of disjunctive invariants,
- the mathematical framework of abstract interpretation, which allows us to precisely formulate the semantics of a toy programming language as well as of the static analyses, and to prove the correctness of the static analyses with regard to the toy programming language.

Teaching methods

The course is composed of 8 lectures and 4 exercises sessions, in which students present examples from exercise sheets, as well as a final presentation, where students present an article from the recent research literature.

List of articles for the final presentation (more to be added according to the number of class participants):Parosh Aziz Abdulla, Bengt Jonsson, Cong Quy Trinh:
Fragment Abstraction for Concurrent Shape Analysis. ESOP 2018: 442-471

WhoHugo Illous, Matthieu Lemerre, Xavier Rival:
Interprocedural Shape Analysis Using Separation Logic-based Transformer Summaries. SAS 2020: 248-273 - Tobias Nießen

Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani:
Improving Thread-Modular Abstract Interpretation. SAS 2021: 359-383

Sifis Lagouvardos, Neville Grech, Ilias Tsatiris, Yannis Smaragdakis:
Precise static modeling of Ethereum "memory". Proc. ACM Program. Lang. 4(OOPSLA): 190:1-190:26 (2020) - Simão Costa

Julian Rosemann, Simon Moll, Sebastian Hack:
An abstract interpretation for SPMD divergence on reducible control flow graphs. Proc. ACM Program. Lang. 5(POPL): 1-31 (2021) - Alice Lee

Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker:
Abstract interpretation of distributed network control planes. Proc. ACM Program. Lang. 4(POPL): 42:1-42:27 (2020) - Aleksei Karasev

Helmut Seidl, Julian Erhard, Ralf Vogler:
Incremental Abstract Interpretation. From Lambda Calculus to Cybersecurity Through Program Analysis 2020: 132-148 - Dominik Apel

Arie Gurfinkel, Jorge A. Navas:
Abstract Interpretation of LLVM with a Region-Based Memory Model. VSTTE 2021: 122-144 -  Alex Loitzl

Mode of examination

Written and oral

Additional information

Lecture Organization (winter term 2022):

Lectures and slides will be videotaped in advance and posted online. The students are asked to watch the videos independently in advance. Questions about the lectures can be discussed in the Q&A sessions. The videos discussed in the Q&A sessions are indicated in the brackets of the respective Q&A session. In order to be able to view the teaching materials, it is necessary to register for the lecture. There are 4 exercise sheets, which are to be solved in advance and to be presented in the practice sessions (by ticking the prepared exercises). The lecture begins with the Q&A session on Oct 6th, 2022, in which the lecture mode will also be discussed again. It is planned to hold the Q&A sessions + exercise sessions + final presentations in person. If necessary due to the pandemic, we will switch to online classes. (Note that the lecture recordings are from WS2021. Hence, the dates in the lecture recordings are not correct.) The exercise session are given by Florian Sextl (https://informatics.tuwien.ac.at/people/florian-sextl).

Lecture start: 6.10.2022 (please watch chapter0, chapter1)

Q&A sessions: 6.10. (chapter0, chapter1), 13.10. (note the different room for this date, chapter2a,chapter2b), 3.11. (chapter3a,chapter3b), 17.11.(chapter4,chapter5), 1.12. (chapter6,chapter7)

Exercises: 27.10., 10.11., 24.11., 15.12.

no session: 20.10., 8.12., 12.1.

The final presentations will be at the end of the semester in January, presumably on 19.1. and 26.1. during the usual lecture times.

Timeline for the presentations:

You need to select a topic before 8.12.

You need to send the outline/first draft of your slides to the exercise coordinator Florian Sextl before 22.12.

You need to meet with Florian Sextl in person/online to discuss/improve the final draft of your finished slides before 13.1.


Static Analylsis Course and Script by Michael Schwartzbach, http://cs.au.dk/~mis/static/
Course on Abstract Interpretation by Patrick Cousot, http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/


"Principles of Program Analysis" by Flemming Nielson, Hanne Riis Nielson, Chris Hankin, 1999

"Principles of Abstract Interpretation" by Patrick Cousot, 2021

"Introduction to Static Analysis - An Abstract Interpretation Perspective" by Xavier Rival and Kwangkeun Yi, 2020

"Term Rewriting and All That", Franz Baader, Tobias Nipkow, chapter 4.8 contains a description of the unfication algorithmus used in the first lecture

"Introduction to lattices and order", B. A. Davey and H. A. Priestley

ECTS Breakdown (3ECTS = 75h): 25h lecture, 25h exercises, 25h presentation



Course dates

Thu10:00 - 12:0006.10.2022 - 26.01.2023Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu10:00 - 12:0013.10.2022FAV Hörsaal 2 Program Analysis
Program Analysis - Single appointments
Thu06.10.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu13.10.202210:00 - 12:00FAV Hörsaal 2 Program Analysis
Thu20.10.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu27.10.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu03.11.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu10.11.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu17.11.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu24.11.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu01.12.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu15.12.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu22.12.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu12.01.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu19.01.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis
Thu26.01.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Program Analysis

Examination modalities

There will be four exercise sheets on the material of the lectures, which are solved by the students and discussed in exercise sessions. The students mark which of the exercises they have been able to solve. The exercise instructor chooses a student among the ones that have marked an exercise for presenting the exercise. Students need to mark 50% of the exercises for successfully passing the course. The exercises do not count towards the final grade. The grade is solely given for the final presentation.

Course registration

Begin End Deregistration end
07.09.2022 12:00 13.10.2022 23:30


Study CodeObligationSemesterPrecon.Info
066 931 Logic and Computation Mandatory elective
066 937 Software Engineering & Internet Computing Mandatory elective
066 938 Computer Engineering Mandatory elective


No lecture notes are available.