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:
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 - Samuel Pilz
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 - Hannes Siebenhandl
Kengo Kido, Swarat Chaudhuri, Ichiro Hasuo:
Abstract Interpretation with Infinitesimals - Towards Scalability in Nonstandard Static Analysis. VMCAI 2016: 229-249 - Stephan Felber
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
