Probabilistic model checking for the data-rich world

Professor Marta Kwiatkowska FRS MAE leads this year’s Lovelace lecture.

She was awarded the 2019 BCS Lovelace Medal for her research in probabilistic and quantitative verification.  Since 2001 she has led the development of the highly influential probabilistic model checker PRISM (



Headline Speaker: Professor Marta Kwiatkowska FRS MAE, University of Oxford

Introductory Speaker: Professor Muffy Calder OBE FREng FRSE, University of Glasgow

Vote of thanks: Professor Tony Cohn, Leeds University



17:45-18:30 - Registration with tea/coffee

18:30 - Lecture commences

20:00 - End of lecture

20:00-21:00 - Networking buffet and drinks reception (optional)

21:00 - Close



Computing systems have become indispensable in our society, supporting us in almost all tasks, from social interactions and online banking to robotic assistants and implantable medical devices. Since software faults in such systems can have disastrous consequences, methods based on mathematical logic, such as proof assistants or model checking, have been developed to ensure their correctness. However, many computing systems employ probability, for example as a randomisation technique in distributed protocols, or to quantify uncertainty in the environment for AI and robotics applications. Systems with machine learning components that make decisions based on observed data also have a natural, Bayesian probabilistic interpretation. In such cases logic no longer suffices, and we must reason with probability.

Probabilistic model checking techniques aim to verify the correctness of probabilistic models against quantitative properties, such as the probability or expectation of a critical event. Exemplified through the software tool PRISM (, they have been successfully applied in a variety of domains, finding and fixing flaws in real-world systems. As today’s computing systems evolve to increasingly rely on automated, strategic decisions learnt from rich sources of data, probabilistic model checking has the potential to provide probabilistic robustness guarantees for machine learning.

Using illustrative examples from mobile communications, robotics, security, autonomous driving and affective computing, this lecture will give an overview of recent progress in probabilistic model checking and highlight challenges and opportunities for the future.



Headline Speaker: Professor Marta Kwiatkowska

Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She is known for fundamental contributions to the theory and practice of model checking for probabilistic systems. She led the development of the PRISM model checker (, the leading software tool in the area. Probabilistic model checking has been adopted in diverse fields, including distributed computing, wireless networks, security, robotics, healthcare, systems biology, DNA computing and nanotechnology, with genuine flaws found and corrected in real-world protocols. Kwiatkowska was awarded two ERC Advanced Grants, VERIWARE and FUN2MODEL, and is a coinvestigator of the EPSRC Programme Grant on Mobile Autonomy. She was honoured with the Royal Society Milner Award in 2018 and the Lovelace Medal in 2019, and is a Fellow of the Royal Society, ACM and BCS, and Member of Academia Europea.

Introductory Speaker: Professor Muffy Calder OBE

Professor Calder is the Professor of Formal Methods, Head of the College of Science and Engineering, and Vice Principal of the University of Glasgow.

Her research is in modelling and reasoning about the behaviour of complex software and biochemical systems using computer science, mathematics and automated-reasoning techniques.

She is one of twelve holders of the Suffrage Science Award in Maths and Computing, presented to celebrate her scientific achievement and her ability to inspire others.

Vote of thanks: Professor Tony Cohn, Leeds University

Professor Tony Cohn holds BSc and PhD degrees from the University of Essex. He spent 10 years at the University of Warwick before moving to Leeds in 1990 where he founded a research group working on knowledge representation and reasoning with a particular focus on qualitative spatial/spatio-temporal  reasoning. His research has broadened to encompass Cognitive Vision, Robotics, Grounding Language in Vision, and Decision Support Systems. He is also a Turing Fellow at the Alan Turing Institute, and is the recipient of the 2015 IJCAI Donald E Walker Distinguished Service Award and the 2012 AAAI Distinguished Service Award. He is a Fellow of the Royal Academy of Engineering, AAAI, AISB,  EurAI, the BCS, and the IET.  He is co-Editor-in-Chief of the journal Spatial Cognition and Computation and has been Chairman/President of AISB, EurAI,  KR inc,  and the IJCAI Board of Trustees. He holds Distinguished Visiting Professor Appointments at Tongji  and Shandong Universities and Qingdao University of Science and Technology.

BCS Lovelace Lecture 2020 - Prof Marta Kwiatkowska
Date and time
24 March, 6:00pm - 9:00pm
The Royal Society
6-9 Carlton House Terrace
5.89 - 32.39 GBP