VSS25: PRISM: Verification under Uncertainty

Wednesday 13th August, Afternoon Session

Talk by Gethin Norman, University of Glasgow and David Parker, University of Oxford

Computerised systems often operate under uncertainty: communication media can be unreliable, hardware components can fail; sensors can yield imprecise information; and protocols may deploy randomisation. PRISM is a tool for automatically verifying the correctness and reliability of such systems, based on formal methods for the construction and analysis of stochastic models. This tutorial will give an introduction to the topic, including some recent advances in the field, and a hands-on guide to getting started with the tool.

BACKGROUND:

PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. It has been used to analyse systems from many different application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, biological systems and many others. PRISM is based on rigorous, mathematical foundations and is particularly well suited to safety-critical applications, from assessing the reliability of airbag control software to building robust controllers for autonomous mobile robots in hazardous environments.

PREPARATION:


Additional materials may be circulated nearer the day, but students are asked to install the latest version of PRISM on their machines in advance.

SPEAKERS:

Dr Sebastian Ullrich headshot

Dr Gethin Norman

Dr Gethin Norman is a Senior Lecturer in the School of Computing Science at the University of Glasgow and a Senior Research Fellow at the Department of Computer Science at the University of Oxford working on the FUN2MODEL: From FUNction-based TO MOdel-based automated probabilistic reasoning for DEep Learning research project. The focus of his research is on the theoretical underpinning of quantitative formal methods, particularly for systems exhibiting real-time and probabilistic behaviour. His recent work has focused on the verification of stochastic concurrent games and partially observable systems. He is a key contributor to the development of the probabilistic verification tool PRISM and together with Marta Kwiatkowska (University of Oxford) and David Parker (University of Birmingham) he was awarded the  the 2016 HVC award for “the invention, development and maintenance of the PRISM probabilistic model checker”. In 2024, they were awarded the ETAPS Test-of-Time Tool Award, also for their tool PRISM.
Dr Sebastian Ullrich headshot

Prof David Parker

I'm a Professor of Computer Science at the University of Oxford and a Tutorial Fellow at Trinity College. From Oct 2021, I am also a Turing Fellow. My research is in formal verification: rigorous techniques for checking that systems function correctly. In particular, I work on quantitative verification methods for checking properties such as safety, reliability, robustness and performance.

I am particularly interested in verification methods for establishing the correctness and robustness of AI-based systems, and work on techniques and tools for providing formally guaranteed solutions to problems across sequential decision making, multi-agent systems and neuro-symbolic systems. I lead the development of PRISM, the most widely-used software tool for verification of probabilistic systems. It was originally created as part of my PhD thesis. See here for some pointers about PRISM, or browse the publications and some applications. We have also developed PRISM-games, an extension of the tool for verifying stochastic games.

I am interested in many aspects of the verification of probabilistic systems. In particular, I currently work on robust verification techniques which can quantify epistemic uncertainty, especially in the context of learning-based systems, and verification of multi-agent systems using stochastic games. I'm interested in applying both to the formal verification and control of AI-driven systems such as robotics and autonomous systems. Take a look at my papers and talks to find out more.