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.

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.

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): 

Gagandeep Singh, Markus Püschel, Martin T. Vechev:
A practical construction for decomposing numerical abstract domains. PACMPL 2(POPL): 55:1-55:28 (2018) - Manuel Reinsperger

Yue Li, Tian Tan, Anders Møller, Yannis Smaragdakis:
A Principled Approach to Selective Context Sensitivity for Pointer Analysis. ACM Trans. Program. Lang. Syst. 42(2): 10:1-10:40 (2020)

Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke:
Fast and exact analysis for LRU caches. Proc. ACM Program. Lang. 3(POPL): 54:1-54:29 (2019) - Lukas Rysavy

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

Mooly Sagiv:
Pointer Analysis of Bytecode Programs for Effective Formal Verification of Smart Contracts. SAS 2021: to appear

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

Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival:
No Crash, No Exploit: Automated Verification of Embedded Kernels. RTAS 2021: 27-39

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)

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)

Lecture Organization (winter term 2021):

Due to Covid-19 the course will be held via distance learning. The setup is as follows:

- there will be pre-recorded videos for each lecture which students are supposed to watch on their own (the lecture slides and recordings are already available online)
- the students are asked to register in order to be able to view the lecture recordings
- the videos are complemented by live Q&A session via ZOOM where students can ask questions about the lectures (in the first Q&A session students can also ask about the setup of the lecture)
- there are 4 exercise sheets which students are supposed to solve on their own and then present their solutions in a live ZOOM session; students need to mark which exercises they are willing to present; for successfully passing the course marking more than 50% of the exercises is required. (all 4 exercise sheets are already online and available for registered students)
- evaluation: each student will give a talk during a live ZOOM session on a recent research paper from the literature; the final grade is solely based on the talk (the date for the presentation is going to be in January, the exact date is to be agreed upon by the lecture participants)

Q&A sessions: 12.10., 9.11.,23.11.,7.12., 13:00-15:00

Exercises: 19.10.,16.11.,30.11.,14.12., 13:00-15:00

Alternative date (if needed): 21.12.

Lecture Start: 12.10. (please watch videos chapter0,chapter1,chapter2).

ZOOM links will be provided via the lecture documents.

Further reading:

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/
The Book Principles of Program Analysis by Flemming Nielson, Hanne Riis Nielson, Chris Hankin

"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

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.