Prof. Dr. Joost-Pieter Katoen

Forschungsschwerpunkte: Formale Methoden, formale Verifikation, probabilistische Modelle, Modellprüfung und Programmverifikation
Joost-Pieter Katoen ist ein theoretischer Informatiker. Seine Forschung ist auf die Entwicklung von mathematischen Verifikationsmethoden zur Bewertung der Genauigkeit von Programmen und Computersystemen gerichtet. Die hierfür verwendeten automatischen Methoden kombinieren Konzepte der mathematischen Logik, der Automaten und der Graphentheorie. Die von ihm entwickelten Techniken und Software-Tools werden in Bereichen wie Sicherheitsanalyse, KI-Planung, Kontrolltheorie, Systembiologie sowie in der modellbasierten Leistungsbewertung und Zuverlässigkeitsanalyse eingesetzt.
Ob in der Forschung, im administrativen oder industriellen Bereich – Software gilt es auf Fehler zu untersuchen. Als einer der weltweit führenden Forschenden im Bereich Formaler Methoden erbringt Joost-Pieter Katoen algorithmisch den Nachweis, dass ein Computersystem den Benutzeranforderungen hinsichtlich Sicherheit genügt und reibungslos funktioniert. Er hat Pionierarbeit im Forschungsgebiet „probabilistisches Model Checking (PMC)“, einem Teilbereich der computergestützten Verifikation, geleistet. Dazu gehören wesentliche Beiträge zu den Grundlagen effizienter, gut skalierbarer Algorithmen für diskrete und zeitkontinuierliche probabilistische Modelle wie die Markov-Entscheidungsprozesse (MDPs). Die heutzutage verfügbaren PMC-Verfahren sind in diversen Teilbereichen adoptiert worden, wie zum Beispiel in der Sicherheitsanalyse, der Planung von Künstlicher Intelligenz und für verteilte randomisierte Algorithmen. Das Softwaretool „Storm“, das von Katoens Team entwickelt wurde, gehört zu den leistungsfähigsten probabilistischen Model Checkern.
Darüber hinaus hat sich Joost-Pieter Katoen in den letzten 15 Jahren der Semantik und Analyse von probabilistischen Programmen gewidmet. Diese Programme können eine sehr breite Klasse von probabilistischen Modellen – das heißt mathematische Modelle, die Zufallsvariablen und Wahrscheinlichkeitsverteilungen mit einschließen – beschreiben. Eingesetzt werden sie unter anderem im Bereich des probabilistischen maschinellen Lernens. Joost-Pieter Katoen konnte insbesondere neue deduktive Verifikationsverfahren für solche Programme entwickeln und teilweise auch automatisieren.
Neben zahlreichen wissenschaftlichen Publikationen veröffentlichte Joost-Pieter Katoen das Buch „Principles of Model Checking“, das in diesem Kontext als Standardwerk gilt.