Gethin Norman

Gethin Norman is a senior lecturer in the School of Computing Science at the University of Glasgow and member of the formal methods research group which is part of the Formal Analysis, Theory and Algorithms research section.

Previously Gethin obtained a degree in mathematics from the University of Oxford and a PhD in computer science from the University of Birmingham. Between 1998 and 2007 he was a Research Fellow in the School of Computer Science at the University of Birmingham and from July 2007 until November 2009, a research officer in the Oxford University Computing Laboratory.

Gethin's research is within the field of formal verification with emphasis on quantitative formal methods, particularly models and algorithms for systems exhibiting real-time and probabilistic behaviour. He is one of the principal developers for the probabilistic verification tool PRISM and its extension to game-based models PRISM-games. PRISM is a software tool for the modelling and analysis of systems whose behaviour exhibits uncertainty or randomness. Example applications include the analysis of the safety of a car's airbag control system, the performance of a Bluetooth-enabled wireless devices and thebehaviour of proteins in a cell. The tool has been used by researchers across the world from fields such as security, robotics, systems biology and quantum cryptography.

Together with Marta Kwiatkowska (University of Oxford) and David Parker (University of Birmingham), he was 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 recognised our "outstanding contributions to probabil