Benjamin Kaminski: Advanced Weakest Precondition Calculi for Probabilistic Programs

 

Ich betreibe Grundlagenforschung für die Entwicklung von Techniken zur automatisierten Analyse und Verifikation probabilitischer Programme. Diese Art von Programmen sind von größter Wichtigkeit in den Feldern Cybersicherheit, Kryptographie, Quantenalgorithmen, Randomisierte Algorithmen und Maschinelles Lernen.

Obwohl probabilistische Programme oft nur aus wenigen Zeilen Quellcode bestehen, beispielweise im Bereich kryptographischer Protokolle, muss ihre Semantik im allgemeinen als Markov-Entscheidungsprozess mit unendlichem Zustandsraum betrachtet werden. Dies lässt ihre Verifikation zu einem hochgradig unentscheidbaren Problem werden. Im Rahmen meiner Forschung betrachte ich solche Entscheidbarkeitsfragen und erforsche außerdem Möglichkeiten, eine möglicht große Teilklasse von probabilistischen Programmen zu identifizieren, die trotz hochgradiger Unentscheidbarkeit des Verifikationsproblems doch analysiert und verifiziert werden können.