concrete program analysis techniques, proof of the correctness of these techniques via abstract interpretation, techniques for developing new program analyses

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;

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:

Sparse Dataflow Analysis with Pointers and Reachability, Anders Møller, Magnus Madsen, SAS 2014

Types as Abstract Interpretations, Patrick Cousot, POPL 1997

An abstract domain to infer ordinal-valued ranking function, Caterina Urban, Antoine Miné, ESOP 2014

Relational thread-modular static value analysis by abstract interpretation, Antoine Miné, SAS 2014

A Correspondence between Two Approaches to Interprocedural Analysis in the Presence of Join, Ravi Mangal, Mayur Naik, Hongseok Yang, ESOP 2014

Byte-Precise Verification of Low-Level List Manipulation, Kamil Dudka, Petr Peringer, Tomáš Vojnar, SAS 2013

Precise Relational Invariants Through Strategy Iteration, Thomas Gawlitza, Helmut Seidl, CSL 2007

Effective Static Race Detection for Java, Mayur Naik, Alex Aiken, John Whaley, PLDI 2006

Escape analysis for Java TM: Theory and practice, Bruno Blanchet, TOPLAS 2003

The talks are going to be in the last week of January this semester (Jan 2016, see lecture slides).