Probabilistische Programme sind herkömmliche Programme mit der Fähigkeit Entscheidungen aufgrund von Zufallsexperimenten zu treffen. Ihre Ausführungen sind daher stochastisch. Im Gegensatz zu anderen nichtdeterministischen Programmen ist es jedoch möglich Aussagen über ihr erwartetes (oder durchschnittliches) Verhalten zu treffen.

Probabilistische Programme finden sich in vielen Anwendungen, z.B. in Form von randomisierten Algorithmen, welche häufig effizienter als ihre deterministischen Alternativen sind, in kryptografischen Protokollen, und als Modellierungssprache für Modelle aus der Statistik und künstlichen Intelligenz.

Das Verhalten von probabilistischen Programmen ist jedoch oft unintuitiv und lässt sich nicht zuverlässig testen. Es ist daher wichtig die Korrektheit von probabilistischen Programmen mit Hilfe formaler Methoden sicherzustellen.

Projekte in dieser Forschungsrichtung beschäftigen sich mit der Entwicklung von Logiken, Methoden und Werkzeugen zur Analyse probabilistischer Programme.

Rust ist eine moderne Systemprogrammiersprache mit einem Schwerpunkt auf Effizienz und Nebenläufigkeit. Dank eines starken Typsystems kann der Rust-Compiler Sicherheitsgarantien geben, die bestimmte Speicherzugriffsverletzungen und Race Conditions ausschließen. Prusti ist eine Erweiterung des Rust-Compilers, die es Entwicklern ermöglicht, ihre Programme mit formalen Spezifikationen zu annotieren und zu verifizieren. Spezifikationsverletzungen werden wie dabei wie jeder andere Fehler des Compilers dargestellt. Prusti nutzt insbesondere das Typsystem von Rust aus, um den manuellen Verifikationsaufwand so weit wie möglich zu reduzieren. Prusti kann somit als ein leichtgewichtiger Ansatz gesehen werden, damit der Rust-Compiler noch stärkere Garantien geben kann.

Projekte in dieser Richtung zielen darauf, Verifikationsansätze für bisher nicht von Prusti unterstützte Merkmale von Rust zu entwickeln. Eine weitere Möglichkeit ist es, Fallstudien zur Softwareverifikation mit Prusti durchzuführen.

Separation Logic ist ein beliebter Formalismus für die Verifikation von Programmen, die (sequentiell oder nebenläufig) Ressourcen, wie z.B. dynamisch allokierten Speicher oder dynamische Datenstrukturen, verwalten. Im Vergleich zur Prädikatenlogik unterstützt Separation Logic zwei Operatoren (die separierende Konjunktion und die separierende Implikation), um solche Ressourcen aufzuspalten und wieder zu kombinieren.

Werkzeuge zur Analyse und Verifikation von Programmen nutzen diese Operationen aus um nur die Resourcen betrachten zu müssen, die für den aktuell betrachteten Programmteil wirklich relevant sind. Der CACM-Artikel von Peter O'Hearn bietet eine ausgezeichnete Einführung.

Ein grundlegendes Problem, welches praktisch jedem automatisierten Ansatz zur Programmverifikation mit Separation Logic zugrunde liegt, ist das Folgerungsproblem: Ist jedes Modell einer gegebenen Formel auch ein Modell einer anderen gegebenen Formel? Obwohl das Folgerungsproblem für Separation Logic im Allgemeinen unentscheidbar ist, hat seine zentrale Rolle in der Verifikation ein großes Interesse an entscheidbaren Fragmenten und unvollständigen Algorithmen ausgelöst.

Projekte in dieser Forschungsrichtung beschäftigen sich damit, Varianten der Separation Logic zu studieren und Werkzeuge zum Lösen des Folgerungsproblems für Fragmente der Separation Logic zu entwickeln.