I am Professor of Computing Systems at the
Oxford University Computing Laboratory and
Professorial Fellow of
Prior to this, I was Professor of Computer Science in the
School of Computer Science
at the University of Birmingham.
My research is concerned with modelling and analysis methods for complex systems,
such as those arising in computer networks, electronic devices and biological organisms.
The analysis methods that I investigate include simulation and formal verification,
and particularly automatic verification (aka model checking).
My work spans the whole spectrum, from theory, through algorithms to software
implementation and applications.
The main focus of my research over the past several years has been on
modelling and verification of probabilistic systems,
which has included both theoretical investigation that resulted in new models and
efficient verification algorithms, as well as practical implementation
using symbolic model checking techniques.
This has culminated in the development of the
PRISM model checker,
which is widely used for the verification of real-world case studies,
ranging from correctness of security protocols, efficiency of wireless protocols,
reliability of nanotechnology designs, to the analysis of signalling pathways.
I lead the Quantitative Analysis and Verification research group, part of the Theory and Automated Verification theme. A (still rather) basic webpage for my group can be found