Marta Kwiatkowska, Gethin Norman and Dave Parker have won the ETAPS Test-of-Time Tool Award 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 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. PRISM is also widely used to support teaching of verification, including at Oxford for the past 15 years.
ETAPS 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 and a presentation given.
