Formal Verification of Randomised Algorithms
On Tuesday 20th of September, we will welcome Joost-Pieter Katoen to Reykjavík University. His lecture; Randomisation is a key concept will be held in room M209
On Tuesday 20th of September, we will welcome Joost-Pieter Katoen for a lecture at Reykjavík University Randomisation is a key concept. It is conceptually simple and can solve certain algorithmic problems quite efficiently. It can treat certain problems in distributed computing for which no deterministic solution does exist. And, random walks are elementary in different fields, e.g., mathematics, physics and economics. In this talk, we will present a formal verification framework to prove the elementary properties of randomisation.
We encode randomisation as probabilistic programs and analyse these programs using a quantitative analogue of a traditional program analysis technique developed by Dijkstra: weakest pre-conditions. We will illustrate how properties such as ``does a random walk terminate almost surely?'', ``does it terminate in a finite number of steps, on average?'', and ``what is the expected (amortised) run-time of a randomised algorithm?'' can be tackled using formal program analysis. We will give some examples of its application and indicate how this can also treat dynamic data structures such as heaps and balanced trees. Finally, the challenges of automating the analysis will be addressed.
Joost-Pieter Katoen is Theodore von Kármán Fellow and Distinguished Professor at RWTH Aachen University, where he is head of the Software Modeling and Verification Group. His research marries theory with its applications and supporting tool development, with a focus on formal methods, computer-aided verification (in particular, model checking), concurrency theory, and semantics (in particular, semantics of probabilistic programming languages). Together with Christel Baier, he wrote and published the book "Principles of Model Checking" (MIT Press), which has received wide acclaim and over 7,100 citations since 2008. Joost-Pieter Katoen was elected a member of Academia Europaea (the Academy of Europe) in 2013. He received an ERC Advanced Grant in 2018 and an honorary doctorate from Aalborg University in 2017.
His paper "Approximate symbolic model checking of continuous-time Markov chains", co-authored with Christel Baier and Holger Hermanns, has been selected for the 2022 CONCUR Test-of-Time Award. Last, but not least, Joost-Pieter Katoen was awarded the FAMOS Prize by RWTH Aachen University in 2017 for his commitment to work-life balance, especially for young PhD students with children.
