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

2022W, VU, 2.0h, 3.0EC

Merkmale

  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: VU Vorlesung mit Übung
  • Format der Abhaltung: Distance Learning

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 (weitere Artikel werden je nach Teilnehmeranzahl hinzugefügt)Parosh Aziz Abdulla, Bengt Jonsson, Cong Quy Trinh:
Fragment Abstraction for Concurrent Shape Analysis. ESOP 2018: 442-471

WhoHugo Illous, Matthieu Lemerre, Xavier Rival:
Interprocedural Shape Analysis Using Separation Logic-based Transformer Summaries. SAS 2020: 248-273

Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani:
Improving Thread-Modular Abstract Interpretation. SAS 2021: 359-383

Sifis Lagouvardos, Neville Grech, Ilias Tsatiris, Yannis Smaragdakis:
Precise static modeling of Ethereum "memory". Proc. ACM Program. Lang. 4(OOPSLA): 190:1-190:26 (2020)

Julian Rosemann, Simon Moll, Sebastian Hack:
An abstract interpretation for SPMD divergence on reducible control flow graphs. Proc. ACM Program. Lang. 5(POPL): 1-31 (2021)

Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker:
Abstract interpretation of distributed network control planes. Proc. ACM Program. Lang. 4(POPL): 42:1-42:27 (2020)

Helmut Seidl, Julian Erhard, Ralf Vogler:
Incremental Abstract Interpretation. From Lambda Calculus to Cybersecurity Through Program Analysis 2020: 132-148

Arie Gurfinkel, Jorge A. Navas:
Abstract Interpretation of LLVM with a Region-Based Memory Model. VSTTE 2021: 122-144

Prüfungsmodus

Schriftlich und Mündlich

Weitere Informationen

Organisation der Vorlesung im WS2021:

Vorlesungen und Folien werden vorab auf Video aufgenommen und online gestellt. Die StudentInnen werden gebeten sich die Videos vorab selbständig anzusehen. Fragen zu den Vorlesungen können jeweils in den Q&A sessions besprochen werden. Die Videos, die in den Q&A sessions besprochen werden, sind in den Klammern der jeweiligen Q&A session angegeben. Um die Unterrichtsmaterialien einsehen zu können, ist es notwendig sich für die Vorlesung anzumelden. Es gibt 4 Übungsblätter, welche vorab zu lösen sind, und die dann in den Übungssessions vorzurechnen sind (mit Ankreuzen der vorbereiteten Übungsaufgaben). Die Vorlesung beginnt mit der Q&A session am 6.10.2022, in der auch der Vorlesungsmodus nochmal besprochen wird. Es ist geplant die Q&A sessions + Übungssessions + Abschlussvorträge in Präsenz abzuhalten, falls aufgrund der Pandemie notwendig, wird auf online Unterricht umgestellt. (Beachten Sie, dass die Vorlesungsaufzeichnungen vom WS2021 stammen. Daher sind die Datumsangaben in den Vorlesungsaufzeichnungen nicht korrekt.)

Vorlesungsbeginn: 6.10.2022 (bitte sehen Sie sich chapter0, chapter1 an)

Q&A sessions: 6.10. (chapter0, chapter1), 13.10. (beachten Sie den anderen Raum für diesen Vorlesungstermin, chapter2a,chapter2b), 3.11. (chapter3a,chapter3b), 17.11.(chapter4,chapter5), 1.12. (chapter6,chapter7)

Übungssessions: 27.10., 10.11., 24.11., 15.12.

keine Vorlesung: 20.10., 8.12., 12.1.

Die Abschlussvorträge finden am Ende des Semesters im Januar statt, vorraussichtlich am 19.1. und 26.1. zur üblichen Vorlesungszeit.

Zeitplan für die Abschlussvorträge:

Sie wählen ein Thema bis zum 8.12.

Sie senden eine Gliederung/ersten Entwurf an den Übungsleiter Florian Sextl bis zum 22.12.

Sie treffen sich mit Florian Sextl persönlich/online um den finalen Entwurf Ihrer fertigen Vortragsfolien zu besprechen/zu verbessern bis zum 13.1.

DIESER ZEITPLAN IST STRIKT!

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/

Books:

"Principles of Program Analysis" by Flemming Nielson, Hanne Riis Nielson, Chris Hankin, 1999

"Principles of Abstract Interpretation" by Patrick Cousot, 2021

"Introduction to Static Analysis - An Abstract Interpretation Perspective" by Xavier Rival and Kwangkeun Yi, 2020

"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 Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Do.10:00 - 12:0006.10.2022 - 26.01.2023Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.10:00 - 12:0013.10.2022FAV Hörsaal 2 Programmanalyse
Programmanalyse - Einzeltermine
TagDatumZeitOrtBeschreibung
Do.06.10.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.13.10.202210:00 - 12:00FAV Hörsaal 2 Programmanalyse
Do.20.10.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.27.10.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.03.11.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.10.11.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.17.11.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.24.11.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.01.12.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.15.12.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.22.12.202210:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.12.01.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.19.01.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse
Do.26.01.202310:00 - 12:00Seminarraum FAV EG C (Seminarraum Gödel) Programmanalyse

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

Von Bis Abmeldung bis
07.09.2022 12:00 13.10.2022 23:30

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Sprache

Englisch