definition of the syntax and semantics of a toy programming language;
simple program analyses, which are used standardly in compilers, such as Reaching Definitions, Live Variable Analysis and Constant Propagation;
program analyses, which are used in program verification such as Interval-, Octagon-, Polyederanalysis for determining program invariants;
advanced program analyses, which are used standardly in compilers, such as Pointer Analysis and Call Graph Analysis;
advanced topics in invariant analysis such as termination- and bound analysis;
the discussed program analyses are defined and proven correct with the technique of abstract interpretation with regard to the earlier defined toy language;
The lecture starts on 3th of Oct.
For further reading I recommond:
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 good description of the unfication algorithmus used in the first lecture
"Introduction to lattices and order", B. A. Davey and H. A. Priestley is a good introduction into lattice theory
ECTS Breakdown (3ECTS = 75h): 25h lecture, 25h exercises, 25h presentation
The participants of this lecture give a talk on a current paper on program analysis.
The participants actively participate in the exercises. At the beginning of each exercise they mark in a table which exercises they are able to present on the blackboard. The participants need to mark 50% of the exercises to pass the lecture.
List of presentation topics:
Alexandru Costan, Stephane Gaubert, Eric Goubault, Matthieu Martel, Sylvie Putot:
A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs. CAV 2005: 462-475
Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, James Worrell:
O-Minimal Invariants for Linear Loops. ICALP 2018: 114:1-114:14
Jiangchao Liu, Liqian Chen, Xavier Rival:
Automatic Verification of Embedded System Code Manipulating Dynamic Structures Stored in Contiguous Regions. IEEE Trans. on CAD of Integrated Circuits and Systems 37(11): 2311-2322 (2018)
Ferdinand, C., Wilhelm, R.: Efficient and precise cache behavior prediction for
real-time systems. Real-Time Syst. 17(2–3), 131–181 (1999)
Patrick Cousot:
Types as Abstract Interpretations. POPL 1997: 316-331
Caterina Urban, Antoine Miné:
An Abstract Domain to Infer Ordinal-Valued Ranking Functions. ESOP 2014: 412-431
Antoine Miné:
Relational Thread-Modular Static Value Analysis by Abstract Interpretation. VMCAI 2014: 39-58
Bhargav S. Gulavani, Sumit Gulwani:
A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis. CAV 2008: 370-384
Christian Müller, Máté Kovács, Helmut Seidl:
An Analysis of Universal Information Flow Based on Self-Composition. CSF 2015: 380-393
Yue Li, Tian Tan, and Yannis Smaragdakis:
Precision-Guided Context Sensitivity for Pointer Analysis. OOPSLA 2018: to appear (https://cs.au.dk/~amoeller/papers/zipper/paper.pdf)
The talks are going to be in the last week of January this semester (Jan 2018, see lecture slides).
