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;
Vorlesungsbeginn ist am 4.10.
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:
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
Die Vorträge finden in der letzten Januarwoche dieses Semesters (Jan 2018, siehe Vorlesungsfolien) statt.
