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
Die Vorlesungsteilnehmer erarbeiten einen Vortrag und schreiben eine Ausarbeitung über ein aktuelles paper aus der Programmanalyse. Liste der Vortragsthemen:
Precise interprocedural dataflow analysis via graph reacability, Reps, Horwitz, and Sagiv, 1995
Points-to analysis with efficient strong updates, Lhotak, Chung, 2011
Semi-sparse flow-sensitive pointer analysis, Hardekopf, Lin, 2009
Parametric shape analysis via 3-valued logic, Sagiv, Reps, Wilhelm, 2002
A parametric segmentation functor for fully automatic and scalable array content analysis, Cousot, Cousot, Logozzo, 2011
Forest automata for verification of heap manipulation, Habermehl, Holík, Rogalwicz, Ji¿í Šimá¿ek und Tomáš Vojnar, 2011
Verification of parameterized concurrent programs by modular reasoning about data and control, Farzan, Kincaid, 2012
Improving strategies via SMT solving, Gawlitza, Monniaux, 2011
Precise interprocedural analysis through linear algebra, Müller-Olm, Seidl, 2004
The octagon abstract domain, Miné, 2006
Combining abstract interpreters, Gulwani, Tiwari, 2006
