BCS Lovelace Lecture 2020/21 – Prof Marta Kwiatkowska

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 Dame Muffy Calder DBE OBE FREng FRSE, University of Glasgow
  • Vote of thanks: Professor Tony Cohn FREng, University of Leeds


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 (prismmodelchecker.org), 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.

Vist the BSC website for more information and to register for the event.