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:
Benno Stein, Benjamin Barslev Nielsen, Bor-Yuh Evan Chang, Anders Møller:
Static analysis with demand-driven value refinement. PACMPL 3(OOPSLA): 140:1-140:29 (2019) - Christoph Hochrainer
Stefan Schulze Frielinghaus, Michael Petter, Helmut Seidl:
Inter-procedural Two-Variable Herbrand Equalities. Logical Methods in Computer Science 13(2) (2017)
Roland Meyer, Sebastian Wolff:
Decoupling lock-free data structures from memory reclamation for static analysis. PACMPL 3(POPL): 58:1-58:31 (2019) - Friedrich Weber
Magnus Madsen, Ming-Ho Yee, Ondrej Lhoták:
From Datalog to flix: a declarative language for fixed points on lattices. PLDI 2016: 194-208 - Vedran Marinkovic
Gagandeep Singh, Markus Püschel, Martin T. Vechev:
A practical construction for decomposing numerical abstract domains. PACMPL 2(POPL): 55:1-55:28 (2018)
Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv:
Simple and precise static analysis of untrusted Linux kernel extensions. PLDI 2019: 1069-1084 - Alexander Graf
Neville Grech, Yannis Smaragdakis:
P/Taint: unified points-to and taint analysis. PACMPL 1(OOPSLA): 102:1-102:28 (2017) - Sarah Sallinger
Oana Fabiana Andreescu, Thomas Jensen, Stéphane Lescuyer, Benoît Montagu:
Inferring frame conditions with static correlation analysis. PACMPL 3(POPL): 47:1-47:29 (2019) - Tom René Hennig
Thomas Gawlitza, Helmut Seidl:
Precise Fixpoint Computation Through Strategy Iteration. ESOP 2007: 300-315 - Samuel Pilz
Meng Wu, Chao Wang:
Abstract interpretation under speculative execution. PLDI 2019: 802-815 - Johann Schiffer
Parosh Aziz Abdulla, Bengt Jonsson, Cong Quy Trinh:
Fragment Abstraction for Concurrent Shape Analysis. ESOP 2018: 442-471 - Hannes Siebenhandl
Kengo Kido, Swarat Chaudhuri, Ichiro Hasuo:
Abstract Interpretation with Infinitesimals - Towards Scalability in Nonstandard Static Analysis. VMCAI 2016: 229-249 - Stephan Felber
The lecture starts on 2nd of Oct.
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