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

2018W, 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

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

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Mi.14:00 - 16:0003.10.2018 - 23.01.2019Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.12:30 - 14:0023.01.2019Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorträge
Programmanalyse - Einzeltermine
TagDatumZeitOrtBeschreibung
Mi.03.10.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.10.10.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.17.10.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.24.10.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.31.10.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.07.11.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.14.11.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.21.11.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.28.11.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.05.12.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.12.12.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.19.12.201814:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.09.01.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.16.01.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.23.01.201912:30 - 14:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorträge
Mi.23.01.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung

Leistungsnachweis

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.

LVA-Anmeldung

Nicht erforderlich

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Sprache

Englisch