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 introduce quantitative verification and illustrate its applicability to several diverse areas, from cellular signalling pathways to protocols for energy management in Microgrids.