2024 ETAPS Test-to-Time Tool Award for PRISM tool by Maria Kwiatkowska
Marta Kwiatkowska, Professor at IPI PAN, and her collaborators Gethin Norman, University of Glasgow, and David Parker, University of Oxford, have been awarded the 2024 ETAPS Test-of-Time Tool Award for their tool PRISM.
PRISM (www.prismmodelchecker.org) is a software tool for modelling and studying the behaviour of real-world systems exhibiting uncertainty or randomness. It has been used for a diverse range of applications, from internet security protocols, to quantum cryptography and 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, deployed for research and teaching worldwide. Over 800 research papers have been published describing the tool, its applications and its extensions. 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 and has been adapted by researchers worldwide. PRISM’s 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.
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.