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 4th 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
Denis Gopan, Thomas W. Reps:
Lookahead Widening. CAV 2006: 452-466
Moritz Sinn, Florian Zuleger, Helmut Veith:
A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis. CAV 2014: 745-761
Daniel Kroening, Matt Lewis, Georg Weissenbacher:
Under-Approximating Loops in C Programs for Fast Counterexample Detection. CAV 2013: 381-396
Laura Kovács:
Reasoning Algebraically About P-Solvable Loops. TACAS 2008: 249-264
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
Jan Strejcek, Marek Trtík:
Abstracting path conditions. ISSTA 2012: 155-165
James C. King:
Symbolic Execution and Program Testing. Commun. ACM 19(7): 385-394 (1976)
Mark Weiser:
Program Slicing. ICSE 1981: 439-449
The talks are going to be in the last week of January this semester (Jan 2018, see lecture slides).
