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.

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):

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

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

Pavol Bielik, Veselin Raychev, Martin T. Vechev:
Learning a Static Analyzer from Data. CAV (1) 2017: 233-253 - Johannes Lindner

Yue Li, Tian Tan, Anders Møller, Yannis Smaragdakis:
A Principled Approach to Selective Context Sensitivity for Pointer Analysis. ACM Trans. Program. Lang. Syst. 42(2): 10:1-10:40 (2020)

Valentin Touzeau, Claire Maïza, David Monniaux, Jan Reineke:
Fast and exact analysis for LRU caches. Proc. ACM Program. Lang. 3(POPL): 54:1-54:29 (2019)

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) - Matthias Hetzenberger

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

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
(https://conf.researchr.org/details/sas-2020/sas-2020-papers/14/Interprocedural-Shape-Analysis-Using-Separation-Logic-based-Transformer-Summaries)

Organisation der Vorlesung:

Aufgrund von Covid-19 wird der Kurs dieses Jahr via distance learning abgehalten. Das Setup ist folgendermaßen:
- die Vorlesungen werden vorab aufgezeichnet und von den StudentInnen selbständig angesehen (es wird 7-8 solcher Vorlesungen geben)
- die aufgezeichneten Videos werden komplementiert durch live Q&A session via ZOOM in welchen die StudentInnen Fragen zu dem Material der Vorlesung stellen können (die erste Q&A session dient auch zu Fragen bezüglich des Vorlesungsmodus)
- es wird 3-4 Übungsblätter geben welche von den StudentInnen bearbeitet und dann in einer live ZOOM session präsentiert werden; die StudentInnen kreuzen an welche Übungen sie präsentieren möchten; für ein erfolgreiches Bestehen des Kurses sind mindestens 50% an angekreuzten Übungsaufgaben erforderlich
- Evaluierung: jede(r) StudentIn hält einen Vortrag zu einem aktuellen Forschungsartikel; die Abschlussnote ensteht nur aus dem Vortrag (das Datum für die Präsentation wird im Januar sein und zusammen mit den Vorlesungsteilnehmern festgelegt)

ZOOM Q&A sessions: 6.10,20.10,3.11.,17.11,1.12., 13:00-15:00

ZOOM Exercise sessions: 27.10.,10.11.24.11,15.12., 13:00-15:00

Die ZOOM links werden über die Vorlesungsnews bekannt gegeben.

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

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.