VSS25: PRISM – DRAFT

Wednesday 13th August, Afternoon Session

Talk by Gethin Norman, University of Glasgow

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.

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.
Dr Sebastian Ullrich headshot

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.