konkrete Programmanalysetechniken, der Nachweis der Korrektheit dieser Analysen mittels Abstrakter Interpretation, Techniken zur Entwicklung neuer Programmanalysen

Defintion von Syntax und Semantik einer Spielzeugsprache;
einfache Programmanalysen, die standardmäßig in Compilern eingesetzt werden, wie Reaching Definitions, Live Variable Analysis und Constant Propagation;
Programmanalysen, die zur Programmverfikation eingesetzt werden, wie Interval-, Octagon-, Polyederanalyse zur Bestimmung von Programminvarianten;
komplexere Programmanalysen, die standardmäßig in Compilern eingesetzt werden, wie Pointer Analysis und Call Graph Analysis;
fortgeschrittene Themen zur Invariantenanalyse, wie Terminations- und Boundanalyse;
die vorgestellten Programmanalysen werden mit der Methode der Abstrakten Interpretation definiert und als korrekt bewiesen, wobei die Spielzeugsprache als Referenzrahmen dient;

Weiterführende Literatur:

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, Kapitel 4.8 enthält eine gute Beschreibung des Unifikationsalgorithmus aus der ersten Vorlesung

"Introduction to lattices and order", B. A. Davey and H. A. Priestley ist eine gute Einführung in Verbandstheorie (lattice theory)

ECTS Breakdown (3ECTS = 75h): 25h Vorlesung, 25h Übung, 25h Vortrag

Die Vorlesungsteilnehmer erarbeiten einen Vortrag über ein aktuelles paper aus der Programmanalyse.

Die Vorlesungsteilnehmer nehmen aktiv an den Übungen teil. Am Anfang jeder Übung kreuzen die Vorlesungsteilnehmer an, welche Aufgaben sie in der Übung präsentieren wollen. Eine erfolgreiche Teilnahme an der Vorlesung erfordert 50% angekreuzte Aufgaben.

Liste der Vortragsthemen:

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

Die Vorträge finden in der letzten Januarwoche dieses Semesters (Jan 2016, siehe Vorlesungsfolien) statt.