Quantitative Verification: Correctness, Reliability and Beyond

Verification techniques such as model checking provide a means to rigorously check the correctness of computerised systems, or to identify flaws in their designs. Quantitative verification generalises this approach by incorporating quantitative aspects of system behaviour such as probability, time, resource usage or rewards. This leads to techniques that check not just correctness, but a variety of quantitative measures such as reliability, performance and many others. This talk will give an introduction to quantitative verification, with a particular focus on probabilistic model checking, a technique for verifying systems with stochastic behaviour. I will provide an overview of this approach, introduce the state-of-the-art probabilistic model checker PRISM, and illustrate its applicability to several diverse areas, from DNA computing designs to protocols for energy management in Microgrids.

Bio:

David Parker is a Lecturer in Computer Science at the University of Birmingham. Prior to that, he was a senior post-doctoral researcher at the University of Oxford. His main research interests are in the area of formal verification, with a particular focus on the analysis of quantitative aspects such as probabilistic and real-time behaviour, and he has published over 90 papers in this area. Recent work includes efficient techniques for scalable verification (e.g. abstraction, compositionality), game-theoretic verification methods, and applications of these approaches to areas such as systems biology, DNA computing and computer security. He leads development of the widely used probabilistic verification tool PRISM, regularly serves on the programme committees of international conferences such as CONCUR, QEST, CMSB and SAC, and frequently gives invited tutorials at summer-schools and workshops.