Achtung ! Wegen eines Fehlers wird derzeit der Studienbeitragsstatus und somit auch der Fortmeldungsstatus falsch angezeigt. An der Behebung des Fehlers wird gearbeitet. Wir danken für Ihr Verständnis!

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

2019W, VU, 2.0h, 3.0EC

Merkmale

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

Lernergebnisse

Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...

- statische Codeanalyse anzuwenden (für Kompilerbau und Programmverifikation),
- neue statische Analysen zu entwickeln,
- die Korrektheit einer Codeanalyse zu beweisen,
- aktuelle Forschungsliteratur aus der Programmanalyse zu rezipieren und zu präsentieren.

Inhalt der Lehrveranstaltung

Die Vorlesung führt in die automatische Programmanalyse ein (wobei wir uns vor allem mit der statischen Codeanalyse auseinandersetzen). Statische Analysen finden sich traditionell im Kompilerbau und werden zur Optimierung des erzeugten Codes eingesetzt. Moderne Entwicklungsumgebungen wie Visual Studio (Aufruf mit dem /analyze flag) und dem Clang Project (Clang Static Analyzer) benützen statische Analysen um mögliche Fehler schon zur Compilezeit zu finden. Dieses Vorgehen wurde beispielweise mit Erfolg in den Entwicklungsprozess von facebook integriert (https://fbinfer.com/). Desweiteren ist statische Analyse ist eine erfolgreiche Methodologie zur Verifikation von Programmen für sicherheitskritische Anwendungen, zum Beispiel um für Flugkontrollsoftware nachzuweisen das bestimmte Laufzeitfehler nicht auftreten können (https://www.absint.com/astree/index.htm).

In der Vorlesung besprechen wir
- einfache statische Analysen, die standardmäßig in Compilern eingesetzt werden, wie Reaching Definitions, Live Variable Analysis und Constant Propagation, sowie komplexere Analysen, wie Pointer Analysis und Call Graph Analysis,
- statische Analysen, die numerische Programminvarianten erzeugen und zur Programmverfikation eingesetzt werden, wie Interval-, Octagon-, Polyederanalyse, sowie Techniken zur Erzeugung disjunktiver Invarianten,
- das mathematische Framework der Abstrakten Interpretation, mit welchem wir sowohl die Semantik einer einfachen Programmsprache als auch von statischen Analysen präzise definieren können, sowie die Korrektheit der statischen Analyse in Bezug auf die zu analysierende Programmiersprachen genau fassen können.

Methoden

Die Lehrveranstaltung setzt sich zusammen aus 8 Vorlesungen und 4 Übungseinheiten, in denen die StudentInnen Aufgaben aus den Übungsblättern präsentieren, sowie Abschlusspräsentationen, in denen die StudentInnen jeweils einen Artikel aus der aktuellen Forschungsliteratur vorstellen.

Liste der Artikel für die Abschlusspräsentation:

Benno Stein, Benjamin Barslev Nielsen, Bor-Yuh Evan Chang, Anders Møller:
Static analysis with demand-driven value refinement. PACMPL 3(OOPSLA): 140:1-140:29 (2019) - Christoph Hochrainer

Stefan Schulze Frielinghaus, Michael Petter, Helmut Seidl:
Inter-procedural Two-Variable Herbrand Equalities. Logical Methods in Computer Science 13(2) (2017)

Roland Meyer, Sebastian Wolff:
Decoupling lock-free data structures from memory reclamation for static analysis. PACMPL 3(POPL): 58:1-58:31 (2019) - Friedrich Weber

Magnus Madsen, Ming-Ho Yee, Ondrej Lhoták:
From Datalog to flix: a declarative language for fixed points on lattices. PLDI 2016: 194-208 - Vedran Marinkovic

Gagandeep Singh, Markus Püschel, Martin T. Vechev:
A practical construction for decomposing numerical abstract domains. PACMPL 2(POPL): 55:1-55:28 (2018)

Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv:
Simple and precise static analysis of untrusted Linux kernel extensions. PLDI 2019: 1069-1084 - Alexander Graf

Neville Grech, Yannis Smaragdakis:
P/Taint: unified points-to and taint analysis. PACMPL 1(OOPSLA): 102:1-102:28 (2017) - Sarah Sallinger

Oana Fabiana Andreescu, Thomas Jensen, Stéphane Lescuyer, Benoît Montagu:
Inferring frame conditions with static correlation analysis. PACMPL 3(POPL): 47:1-47:29 (2019) - Tom René Hennig

Thomas Gawlitza, Helmut Seidl:
Precise Fixpoint Computation Through Strategy Iteration. ESOP 2007: 300-315

Meng Wu, Chao Wang:
Abstract interpretation under speculative execution. PLDI 2019: 802-815 - Johann Schiffer

Parosh Aziz Abdulla, Bengt Jonsson, Cong Quy Trinh:
Fragment Abstraction for Concurrent Shape Analysis. ESOP 2018: 442-471

Kengo Kido, Swarat Chaudhuri, Ichiro Hasuo:
Abstract Interpretation with Infinitesimals - Towards Scalability in Nonstandard Static Analysis. VMCAI 2016: 229-249

Prüfungsmodus

Schriftlich und Mündlich

Weitere Informationen

Vorlesungsbeginn ist am 2.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 Beschreibung des Unifikationsalgorithmus aus der ersten Vorlesung

"Introduction to lattices and order", B. A. Davey and H. A. Priestley ist eine 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:0002.10.2019 - 29.01.2020Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.12:30 - 14:0022.01.2020Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorträge
Mi.12:30 - 14:0029.01.2020Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorträge
Programmanalyse - Einzeltermine
TagDatumZeitOrtBeschreibung
Mi.02.10.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.09.10.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.16.10.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.23.10.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.30.10.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.06.11.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.13.11.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.20.11.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.27.11.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.04.12.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.11.12.201914:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.08.01.202014:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.15.01.202014:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.22.01.202012:30 - 14:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorträge
Mi.22.01.202014:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung
Mi.29.01.202012:30 - 14:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorträge
Mi.29.01.202014:00 - 16:00Seminarraum FAV EG B (Seminarraum von Neumann) Programmanalyse - Vorlesung

Leistungsnachweis

Es gibt vier Übungsblätter zu den Inhalten der Vorlesung, die von den StudentInnen bearbeitet und anschließend in jeweils einer Übungsstunde besprochen werden. Die StudentInnen kreuzen an welche Übungsbeispiele sie bearbeitet haben. Aus diesen StudentInnen wählt der Übungsleiter jeweils eine Studentin/einen Studenten der/die das Übungsbeispiel präsentiert. StudentInnen müssen 50% der Aufgaben ankreuzen für das positive Abschließen der Lehrveranstaltung. Die Übungen fließen allerdings nicht in die Abschlussnote mit ein. Die Abschlussnote ergibt sich nur aus dem Abschlussvortrag. 

LVA-Anmeldung

Nicht erforderlich

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Sprache

Englisch