Professor Dr Joost-Pieter Katoen

Research Priorities: Formal methods, formal verification, probabilistic models, model checking, and program verification
Joost‐Pieter Katoen is a theoretical computer scientist. His work focuses on the development of mathematical verification methods for assessing the accuracy of programs and computer systems. The automatic methods used for this combine concepts of mathematical logic, automata and graph theory. His developed techniques and software tools are applied in areas such as safety analysis, AI planning, control theory, system biology, and in model‐based performance assessment and reliability analyses.
Be it in research or in the administrative or industrial sectors, software needs to be examined for errors. As one of the world’s leading researchers in the field of formal methods, Joost‐Pieter Katoen uses algorithms to show that a computer system meets safety requirements and is running efficiently. He has carried out pioneering research in the field of “probabilistic model checking (PMC)”, a branch of computer‐assisted verification. This includes significant contributions to the foundational aspects of efficient, well‐scalable algorithms for discrete- and continuous-time probabilistic models such as Markov decision processes (MDPs). PMC software tools available today have been adopted in a wide variety of areas, including security analysis, AI planning, and distributed randomised algorithms. The software tool Storm, developed by Katoen’s team, is one of the most powerful probabilistic model checkers.
Over the last 15 years, Joost‐Pieter Katoen has also focused on the semantics and analysis of probabilistic programs. Such programs can describe a very broad range of probabilistic models, i.e.
mathematical models that include stochastic variables and probability distributions. They are used in fields such as security and probabilistic machine learning. In particular, Joost‐Pieter Katoen has been able to develop and partially automate new deductive verification processes for such programs.
In addition to numerous scientific publications, Joost‐Pieter Katoen co‐authored the book “Principles of Model Checking”, which is considered a standard reference text in the field.