Unsere Forschung verbindet die mathematischen Grundlagen von Programmen, Programmiersprachen und Rechensystemen mit automatischer Analyse und Verifikation. Gerade weil KI-Systeme zunehmend Code erzeugen, werden Verfahren wichtiger, die Korrektheit, Sicherheit und Ressourcenverbrauch unabhängig überprüfen können. Wir entwickeln dafür Modelle, Logiken, Algorithmen und Werkzeuge, setzen maschinelles Lernen zur Unterstützung des automatischen Schließens ein und nutzen logische Methoden, um die Möglichkeiten und Grenzen von KI-Modellen zu charakterisieren.
Was bedeutet ein Programm?
Formale Semantiken und Typsysteme beschreiben präzise, was Programme bedeuten und welche Programme zulässig sind. Wir untersuchen insbesondere, wie moderne Programmiersprachen Sicherheit gewährleisten.
Ausgewählte Themen:
- Formale Semantik und Typsysteme
- Formale Modelle von Ownership und Borrowing
- Formale Methoden für die Programmiersprache Rust
Wie lassen sich Programme automatisch analysieren?
Wir entwickeln Verfahren, die Eigenschaften von Programmen automatisch herleiten und für die Verifikation nutzbar machen.
Ausgewählte Themen:
- Kompositionelle Shape Analysis zur Verifikation von Speichersicherheit
- Separation-Logic-basierte Programmanalyse und Biabduktion
- Automatische Herleitung von Ressourcen- und Komplexitätsschranken
Was lässt sich automatisch entscheiden?
Wir untersuchen die Ausdrucksstärke, Entscheidbarkeit und Komplexität von Logiken, Automaten und anderen mathematischen Modellen.
Ausgewählte Themen:
- Ausdrucksstärke und Entscheidbarkeit von Fragmenten der Separation Logic
- Petri-Netze beziehungsweise Vektoradditionssysteme (VASS) und verwandte unendliche Zustandssysteme
- Automaten und logische Formalismen für Graphen und Rechensysteme
Wie können formale Methoden und KI voneinander profitieren?
Maschinelles Lernen kann formale Verfahren unterstützen; umgekehrt können logische Methoden helfen, KI-Modelle zu verstehen.
Ausgewählte Themen:
- Maschinell erlernte Heuristiken für die Beweissuche in Prädikatenlogik erster Stufe
- Logische Charakterisierungen der Ausdrucksstärke neuronaler Netze
- Entwicklung von ML-Modellen auf Grundlage logischer Charakterisierungen