Programmiersprachen und Verifikation

Jun.-Prof. Dr. Kevin Batz

Forschung

Unsere Forschung liegt an der Schnittstelle von Verifikation, automatisiertem Schließen und mathematischer Logik. Wir entwickeln Logiken und Verfahren zur Verifikation und Synthese probabilistischer und allgemeiner quantitativer Systeme – insbesondere parametrischer Systeme und solcher mit unendlich vielen Zuständen. Eine zentrale Frage ist dabei, in welchem Umfang sich das Schließen über ihr Verhalten automatisieren lässt, auch wenn dieses durch Unsicherheit oder Nichtdeterminismus geprägt ist.

Dazu nutzen wir quantitative Programmlogiken, automatisierte Beweissuche, Satisfiability Modulo Theories (SMT), Synthese und aktives Lernen. Mit interaktiven Theorembeweisern wie Lean 4 formalisieren und überprüfen wir außerdem die mathematischen Argumente, auf denen diese Methoden beruhen.

Unsere Forschung verbindet theoretische Grundlagen mit der Entwicklung praktisch nutzbarer Softwarewerkzeuge. Dabei geht es darum, semantische Konzepte in Verfahren zu übersetzen, die komplexe Systeme analysieren, ihre Korrektheit nachweisen oder Systeme mit gewünschten Eigenschaften automatisch erzeugen können. Anwendungen reichen vom Korrektheitsnachweis randomisierter Algorithmen bis zur Untersuchung der Zuverlässigkeit von Computernetzwerken oder Netzwerktopologien in Rechenzentren unter unsicheren Bedingungen.