Prof Marta Kwiatkowska

Marta Kwiatkowska has been Professor of Computing Systems at Oxford University Computing Laboratory and Fellow of Trinity College since 2007. Prior to this she held academic positions at the Universities of Birmingham, Leicester and the Jagiellonian University in Cracow, Poland.

Marta Kwiatkowska’s research is concerned with modelling and formal verification for complex systems, such as those arising in computer networks, electronic devices and biological organisms. The main focus is on automatic verification via model checking, a technique whose founders were recently recognized by the prestigious ACM 2007 Turing Award. Model checking aims to establish, by means of an algorithm, whether certain properties hold for a system model, typically represented as a state-transition graph. The advantage of model checking is that it explores all system executions and, unlike testing, amounts to a mathematical proof. Examples of properties of interest are safety (e.g. “the car will never stall while driving autonomously” for intelligent vehicles) and security (e.g. “my PIN will never be revealed to another customer” for online banking). Model checking thus helps to ensure the safe, secure, reliable and resource-efficient operation of computing systems.

Kwiatkowska spearheaded the development of quantitative probabilistic model checking techniques on the international scene. Probabilistic model checking techniques are of great relevance not only in computer science, but also in many areas of science and engineering. System models in this case are variants of Markov chains, and can be thought of as state-transition graphs appropriately annotated with quantities to represent timing delays, probability of taking an action, or power usage. The properties of interest have quantitative outcomes; examples include probability (e.g. “what is the probability that my PIN can be compromised” for online banking) and energy efficiency (“what is the expected power consumption during the first hour of autonomous operation” in an intelligent vehicle). As in conventional model checking, quantitative model checking explores all system executions, and is thus able to identify worst- and best-case scenarios not feasible with analysis methods such as simulation.

Kwiatkowska’s work spans the full spectrum, from theory, through algorithms to software implementation and applications. She led the development of the first and internationally leading probabilistic symbolic model checker PRISM (www.prismmodelchecker.org), widely used for research and teaching. This involved the formulation of new models and state-of-the-art verification algorithms, as well as implementation and application of the techniques in practice. PRISM has been used to model and analyse, in several cases detecting design errors, a wide range of real-world systems: wireless, security and anonymity protocols, distributed coordination protocols, nanotechnology designs, web-services, power management schemes and molecular signalling pathways.

Marta Kwiatkowska currently holds £2.2m of research funding from EPSRC and EU addressing topics related to quantitative modelling and verification in ubiquitous computing, sensor networks, large-scale IT systems, component-based architectures and fault-tolerant software. Her work on the theory to practice transfer of probabilistic model checking was recognised by invitation to speak at the leading LICS 2003 and ESEC/FSE 2007 conferences. Kwiatkowska was lead organiser of the Royal Society Discussion Meeting "From computers to ubiquitous computing, by 2020" and guest co-editor of the associated Proceedings in Phil. Trans. R. Soc. A vol 366 no 1881.