His expertise is in formal verification, in particular for probabilistic systems. He has made significant contributions, covering theory, algorithms and tools and has a proven track record for applying these to novel application domains, co1 winning the 2016 HVC award for “most influential work in the last 5 years in formal verification”. He has published 150+ papers in these areas with a wide network of collaborators, and has served on the PC for 60+ international conferences, 3 as chair. As of 2021, he is a Turing Fellow, providing access to a further extensive network of researchers. He manages development of the open source, internationally-leading PRISM verification tool and his projects have been funded by EPSRC, EU/ERC and DARPA.