Time Award for Marta Kwiatkowska and David Parker's PRISM Software Tool

Trinity Professorial Fellow Marta Kwiatkowska and Tutorial Fellow Dave Parker have been awarded the 2024 ETAPS Test-of-Time Tool Award with their colleague Gethin Norman of Glasgow University for their tool PRISM.

PRISM is a software tool for modelling and analysing the behaviour of real-world systems whose behaviour exhibits uncertainty or randomness. It has been used to study a diverse range of applications, from internet security protocols, to quantum cryptography to protein interactions in the human cell. 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 is open source software that has been in continuous development for over 20 years and is the most widely used tool of its kind. It has been used in industrial projects and labs, from cloud computing at Fujitsu to fault-tolerant architectures at Honeywell and airbag safety at TRW Automotive. 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. PRISM is also widely used to support teaching of verification, including at Oxford for the past 15 years.

ETAPS – the European joint conferences on theory and practice of software – is the primary European forum for academic and industrial researchers working on topics relating to software science, and has been running for over 25 years. The ETAPS Test-of-Time Tool Award was initiated to recognise “the importance of reliable and well-maintained research tools and the significant effort that their creation and maintenance entails”. It acknowledges tools that have a lasting effect on the community. ETAPS 2024 was held in Luxembourg, where the award was presented.