Proseminar: Abstrakte Interpretation
LSF: tba
Moodle: tba
Das Proseminar wird in deutscher Sprache gehalten.
Inhalt
Abstrakte Interpretation ist eine Methode der statischen Programmanalyse. Wie alle Methoden in diesem Bereich ist sie in der Lage, Eigenschaften von Programmen abzuleiten, ohne sie (oder bevor sie) ausgeführt werden. Die praktischen Anwendungen hierfür sind zahlreich und haben immer wieder ihre Nützlichkeit für Compiler-Optimierungen (z.B. für schnellere Programme), Sicherheit (z.B. werden meine persönlichen Daten weitergegeben) oder Schutz (z.B. treten die Bremsen automatisch rechtzeitig an, wenn der Näherungssensor meines Autos eine Wand wahrnimmt) gezeigt.
Formal gesehen ist die abstrakte Interpretation eine solide Annäherung an die Semantik von Computerprogrammen, die auf monotonen Funktionen über geordneten Mengen, insbesondere Verbänden, basiert. Hilft Ihnen diese Definition weiter? Wahrscheinlich nicht. Versuchen wir also etwas anderes: Abstrakte Interpretation ist eine Ausführung des Programms, die nicht mit tatsächlichen Werten arbeitet, sondern mit Abstraktionen, die Sie kontrollieren. Anstatt sich also an eine tatsächliche ganze Zahl zu erinnern, merken Sie sich einfach, ob es ein positiver oder negativer Wert ist, wenn das es ist, was Sie interessiert.
In diesem Seminar werden wir - Schritt für Schritt - das Feld der abstrakten Interpretation erkunden, indem wir sowohl klassische Texte als auch aktuelle Veröffentlichungen zu diesem Thema lesen. Es wird eine spannende Reise für alle, die sich dafür interessieren, wie Programme funktionieren und was wir über sie aussagen können, wenn wir sie "nur anschauen". Man muss allerdings ein bisschen Mathematik verstehen und sich mit Funktionen, griechischen Buchstaben und dergleichen auskennen. Es ist, was es ist.
Form
Das Proseminar wird in Form eines "Diskussionsseminars" abgehalten. Dabei treffen sich alle Seminarteilnehmende zweiwöchentlich zu einer Sitzung, bei der nach einer kurzen Einleitung ein bestimmter Themenbereich frei diskutiert wird. Zu jeder Sitzung sind entsprechende Paper durchzuarbeiten, die vorher bekanntgemacht werden. Zu jedem Paper bereitet ein Seminarteilnehmer eine Kurzpräsentation vor (~10 min), die zu Anfang der entsprechenden Sitzung vor dem Seminar vorgestellt wird. Die Abschlussnote für das Proseminar bewertet die Qualität der Diskussionsbeiträge, die Kurzpräsentation sowie eine kurze schriftliche Ausarbeitung, die am Ende des Seminars anzufertigen ist.