Posted: 5th July 2016

Marta Kwiatkowska (University of Oxford), Gethin Norman (University of Glasgow) and Dave Parker (University of Birmingham) have been given the 2016 HVC award for "the invention, development and maintenance of the PRISM probabilistic model checker".

The HVC award is given to the most influential work in the last five years in formal verification, simulation, and testing. The committee awarded Marta Kwiatkowska, Gethin Norman and Dave Parker for their work on PRISM, recognising "their outstanding contributions to probabilistic model checking and, more generally, to formal verification".

PRISM (see www.prismmodelchecker.org ) is a software tool for modelling and studying the behaviour of real-life systems whose behaviour exhibits uncertainty or randomness. It can be used to analyse everything from the the safety of a car's airbag control system, to the performance of a Bluetooth-enabled wireless device, to the behaviour of proteins in the human cell. PRISM has been used by researchers worldwide in fields as diverse as computer security, robotics, systems biology and quantum cryptography. 

The tool has been in continuous development for over 15 years, has been downloaded more than 50,000 times, and almost 500 research papers have been published about its usage and development.

HVC Award announcement https://www.research.ibm.com/haifa/conferences/hvc2016/award.shtml 

PRISM website  http://www.prismmodelchecker.org