Software durchdringt alle Bereiche der modernen Gesellschaft. Automatisches Schlussfolgern über Programme ist wesentlich für ihre Korrektheit, Zuverlässigkeit und Vertrauenswürdigkeit und gewinnt weiter an Bedeutung, da zunehmend Code maschinell erzeugt wird. Wir untersuchen die mathematischen Grundlagen von Programmen, Programmiersprachen und Rechensystemen und entwickeln Modelle, Logiken, Algorithmen und Werkzeuge, mit denen sich ihre Eigenschaften automatisch analysieren und verifizieren lassen.

Forschung

Unsere Forschung umfasst vier eng miteinander verbundene Schwerpunkte:

• Grundlagen von Programmen und Programmiersprachen: präzise mathematische Modelle, formale Semantiken und Typsysteme sowie Konzepte wie Ownership und Borrowing; ein aktueller Schwerpunkt liegt auf der Programmiersprache Rust
• Programmanalyse und Softwareverifikation: statische Analyse, automatische Terminierungs-, Ressourcen- und Komplexitätsanalyse sowie Separation Logic und Shape Analysis zur Verifikation von Speichersicherheit
• Logik, Automaten und unendliche Zustandssysteme: Ausdrucksstärke, Entscheidbarkeit und Komplexität von Logiken, Automaten und verwandten mathematischen Modellen, darunter Vektoradditionssysteme (Petri-Netze) und Graphgrammatiken
• Formale Methoden und Künstliche Intelligenz: Einsatz maschinellen Lernens zur Unterstützung des automatischen Schließens sowie logische Methoden zum Verständnis von KI-Modellen; aktuelle Themen sind maschinell erlernte Heuristiken für die Beweissuche und logische Charakterisierungen neuronaler Netze

Lehre

Unsere Lehre umfasst die Grundlagen der Programmierung sowie weiterführende Themen aus den Bereichen Programmiersprachen, Programmanalyse und formale Methoden. Dazu gehören funktionale Programmierung, Compilerbau, Programmoptimierung und Programmverifikation ebenso wie Logik, Automatentheorie und automatisches Schließen.

Informationen zu den aktuell angebotenen Lehrveranstaltungen finden sich unter Lehre.

Zusammenarbeit

Wir betreuen Bachelor- und Masterarbeiten in allen genannten Bereichen und besprechen gerne auch Themen, die nicht auf unserer aktuellen Liste stehen. Siehe Themen für Abschlussarbeiten.

Wir freuen uns außerdem über Anfragen von Promotionsinteressierten mit einem Hintergrund in Logik und Automatentheorie, Programmiersprachen, Programmanalyse, Verifikation oder theoretischem maschinellem Lernen sowie über Anfragen zu Forschungskooperationen.