Talk by Gethin Norman, University of Glasgow and David Parker, University of Oxford
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.
PRISM has been in continuous development for over 20 years and is the most widely used tool of its kind. Over 850 research papers have been published describing the tool, its applications and projects that build upon it. It has also been used in industrial projects and labs, from cloud computing at Fujitsu to fault-tolerant architectures at Honeywell and airbag safety at TRW Automotive.
PRISM is open source software and has been adapted and enhanced by researchers worldwide. Its modelling language has become a de facto standard for representing probabilistic models within the formal verification community, and has been adopted and extended by many other tools.
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.
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.
by