184.703 Programmanalyse
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2011W, VU, 2.0h, 3.0EC

Merkmale

  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: VU Vorlesung mit Übung

Ziele der Lehrveranstaltung

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

Inhalt der Lehrveranstaltung

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;

Weitere Informationen

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

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Di.17:00 - 18:0018.10.2011Seminarraum FAV EG B (Seminarraum von Neumann) Vorbesprechung
Di.12:00 - 13:3008.11.2011 - 24.01.2012Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Programmanalyse - Einzeltermine
TagDatumZeitOrtBeschreibung
Di.18.10.201117:00 - 18:00Seminarraum FAV EG B (Seminarraum von Neumann) Vorbesprechung
Di.08.11.201112:00 - 13:30Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Di.22.11.201112:00 - 13:30Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Di.29.11.201112:00 - 13:30Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Di.06.12.201112:00 - 13:30Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Di.13.12.201112:00 - 13:30Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Di.20.12.201112:00 - 13:30Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Di.10.01.201212:00 - 13:30Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Di.17.01.201212:00 - 13:30Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung
Di.24.01.201212:00 - 13:30Seminarraum FAV EG C (Seminarraum Gödel) Vorlesung

Leistungsnachweis

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

LVA-Anmeldung

Nicht erforderlich

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Sprache

Englisch