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