HVC Award

The HVC award is given to the most influential work in the last five years in formal verification, simulation, and testing. The award is not limited to influential articles; it can also be a system or a collection of activities that promote the area.

The HVC award committee has decided to give the award this year to Prof. Marta Kwiatkowska (University of Oxford), Dr. Gethin Norman (University of Glasgow) and Dr. Dave Parker (University of Birmingham), for the invention, development and maintenance of the PRISM probabilistic model checker.

The PRISM formal verification tool supports modelling and analysis of systems with probabilistic behaviour. It complements more traditional formal verification tools with the capability to analyze quantitative properties. Application areas include communication protocols, security protocols, randomized distributed algorithms, biological and chemical systems, cyber-physical systems and human-robot interaction. The PRISM model checker is widely used by the scientific community, both within and outside of the CS community.

By awarding Prof. Marta Kwiatkowska, Dr. Gethin Norman and Dr. Dave Parker, the committee recognizes their outstanding contributions to probabilistic model checking and, more generally, to formal verification.

HVC Award Committee

• Leonardo Mariani, chair (University of Milano Bicocca)
• Armin Biere (Johannes Kepler University)
• Hana Chockler, (King's College London)
• Kerstin Eder (University of Bristol)
• Andrey Rybalchenko (Microsoft Research)
• Ofer Strichman (Technion)