The focus of his research is on the theoretical underpinning of quantitative formal methods, particularly for systems exhibiting real-time and probabilistic behaviour. He is a key contributor to the development of PRISM, has over 100 peer-reviewed publications and served on over 50 PC committees for international conferences and workshops. His recent work has focused on the verification of stochastic concurrent games and partially observable systems. Together with Dave Parker and Marta Kwiatkowska, he received the 2016 HVC award for the most influential work in the last five years in formal verification, simulation and testing.