Prof. Joost-Pieter Katoen
Biography
Joost-Pieter Katoen (M'15) is a Distinguished Professor with RWTH Aachen University, Aachen, Germany, and holds a part-time professorship at the University of Twente, Enschede, The Netherlands. He is a member of Academia Europaea and received a honorary doctorate degree from Aalborg University, Aalborg, Denmark. He has been visiting professor at a.o. the University of Oxford, IST Austria, and Macquarie University in Sydney. His research interests include formal methods, model checking, concurrency theory, and probabilistic computation. In 2018, he received an ERC Advanced Research Grant. He coauthored more than 170 conference papers, 70 journal papers, and the book on "Principles of Model Checking". Prof. Katoen is the Chairman of the steering committee of ETAPS, and steering committee member of the conferences CONCUR, QEST, and FORMATS.
Abstract
Probabilistic programming combines probability theory, statistics and -- most importantly from a modeling point of view -- programming languages. They allow to model a much larger class of models in a rather succinct manner. The full potential of modern probabilistic programming languages comes from automating the process of inferring unobserved variables in the model conditioned on observed data. As some researchers put it: "The goal of probabilistic programming is to enable probabilistic modeling and machine learning to be accessible to the working programmer."
Probabilistic programs steer autonomous robots, are at the heart of security mechanisms, encompass randomised algorithms, and are used in AI to infer statistical conclusions about huge amounts of uncertain data.
In this series of lectures, I will introduce the main concepts of probabilistic programming, and discuss how classical program verification a la Dijkstra can be used to answer questions such as: Do these programs compute what one expects them to do? Do they terminate at all? With what probability? How much resources do they consume? Applications to Bayesian networks will show how insightful information about analysing such networks can be obtained in a fully automated manner by using program verification.