I graduated with BSc and MSc in Computer Science from the Jagiellonian University, Cracow, Poland, which I subsequently joined as Junior Assistant Professor before moving to the University of Leicester to study for my doctorate, also in Computer Science. I continued at the University of Leicester as a Lecturer, and then moved to the University of Birmingham, where I was promoted to full Professorship. Since 2007, I have held a Statutory Chair in the Department of Computer Science at Oxford and a Professorial Fellowship of Trinity College. I was elected to Academia Europea and Fellowship of the BCS, and have held a number of senior academic appointments, including membership of the 2014 REF (Research Assessment Framework) Panel and chairing the ERC (European Research Council) Starting Grants Panel.
I teach undergraduates and MSc students in the Department of Computer Science and advise graduate students at Trinity. The course on ‘Probabilistic Model Checking’ that I teach currently is an introduction to my research, and it includes both theory and practical work using the probabilistic model checker PRISM developed in my group. I am also involved in two Centres for Doctoral Training, AIMS (Autonomous Intelligent Machines and Systems) and Synthetic Biology. In addition, I frequently give tutorials about my research at summer schools (see my personal webpage).
I hold the ERC Advanced Grant VERIWARE awarded to ‘exceptional research leaders’, one of only 7 awarded in Europe in 2010.
Computing infrastructure has become indispensable in our society, with examples ranging from online banking, to intelligent vehicles and electronic medical equipment. Software faults in such systems can have disastrous consequences.
My research is concerned with developing modelling and automated verification techniques that can guarantee the stable, safe, secure, timely, reliable and resource-efficient operation of computing systems. Model checking is a verification technique that can establish whether certain properties, usually expressed in temporal logic, hold for a system model. The models describe how systems move between states by executing actions, and are typically represented as state-transition graphs. Model checking explores all system executions and, unlike testing, amounts to a mathematical proof. This task is inherently challenging in view of infinite state spaces and undecidability of the underlying problem. In conventional model checking, the properties of interest are qualitative, such as safety (e.g. ‘the car will never stall while driving autonomously’ for intelligent vehicles). The distinctive aspect of my work is its focus on probabilistic and quantitative verification techniques.
I led the development of the leading international probabilistic symbolic model checker PRISM, which has been downloaded over 40,000 times and used to analyse over 90 case studies, discovering flaws in several of them. PRISM systematically explores a model of a system against properties such as ‘what is the worst case time to deliver an update from the sensor monitoring distance to the car ahead?’ (for an intelligent vehicle) and ‘what is the expected power consumption during the first hour of operation?’ (in a body-sensor network). PRISM has proved its usefulness in many distinct fields, including distributed and cloud computing, wireless networks, security, robotics, quantum computing, game theory, biology and nanotechnology.
- From Software Verification to ‘Everyware’ Verification
- DNA walker circuits: computational potential, design, and verification
- On Quantitative Software Quality Assurance Methodologies for Cardiac Pacemakers
- Automatic Verification of Competitive Stochastic Systems
- A Compositional Specification Theory for Component Behaviours
- PRISM 4.0: Verification of Probabilistic Real-time Systems