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.
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 - Tobias Nießen
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) - Simão Costa
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) - Alice Lee
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) - Aleksei Karasev
Helmut Seidl, Julian Erhard, Ralf Vogler:
Incremental Abstract Interpretation. From Lambda Calculus to Cybersecurity Through Program Analysis 2020: 132-148 - Dominik Apel
Arie Gurfinkel, Jorge A. Navas:
Abstract Interpretation of LLVM with a Region-Based Memory Model. VSTTE 2021: 122-144 - Alex Loitzl
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.) Die Übungstermine werden von Florian Sextl abgehalten ((https://informatics.tuwien.ac.at/people/florian-sextl).
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
