On Quantitative Software Verification

Prof. Marta Kwiatkowska

Professor of Computing Systems

University of Oxford

Abstract:

The vast majority of software verification research to date has concentrated on qualitative analysis methods, for example the absence of safety violations in program executions. Many programs, however, contain randomisation, timing and resource information. Quantitative verification is a technique for establishing quantitative properties of a system model, such as the probability of battery power dropping below minimum, the expected time for message delivery and the expected number of messages lost before protocol termination. Tools such as the probabilistic model checker PRISM (www.prismmodelchecker.org) are widely used in several application domains, including security and network protocols, but their application to real software is limited.

This lecture presents recent results concerning quantitative software verification for ANSI-C programs extended with random assignment. The goal is to focus on system software that exhibits probabilistic behavior and properties such as “the maximum probability of file-transfer failure”, or “the maximum expected number of failed transmissions”. We use a quantitative abstraction-refinement framework based on predicate abstraction, in which probabilistic programs are represented as Markov decision processes and their abstractions as stochastic two-player games. These techniques have been implemented using components from GOTO-CC, SATABS and PRISM and successfully used to verify actual networking software.

Biography:

Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She was elected to Academia Europea and received a prestigious ERC Advanced Grant VERIWARE "From software verification to everyware verification", 2010-15.

Kwiatkowska's research is concerned with modelling and verification techniques for probabilistic systems, with application to engineered and biological systems. She spearheaded the development of probabilistic and quantitative methods in verification on the international scene. Her work on the theory to practice transfer of probabilistic model checking was recognised by invitations to speak at the LICS 2003 and ESEC/FSE 2007 conferences. She led the development of the PRISM model checker (www.prismmodelchecker.org), the leading software tool in the area and widely used for research and teaching. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management and systems biology. Her research is currently supported by £3.7m of grant funding from EPSRC, EU, DARPA, Oxford Martin School and Microsoft Research.

Kwiatkowska serves on editorial board of IEEE Transactions on Software Engineering, Philosophical Transactions of the Royal Society A and Science of Computer Programming, and has lectured at several summer schools, including ESSLLI and the Marktoberdorf Summer School.