Probabilistic model checking is an algorithmic method for establishing the correctness of probabilistic systems, for example randomised algorithms or software that exhibits failures. Systems such as these, which exhibit both probabilistic and nondeterministic behaviour are naturally modelled using Markov decision processes (MDPs). Specifications given in probabilistic temporal logic, expressing quantitative properties such as the "the maximum probability of file-transfer failure" can be verified automatically and efficiently.
Probabilistic model checking of large, complex systems, such as software, necessitates the use of abstraction techniques. We have proposed the use of two-player stochastic games as abstractions for MDPs and have a developed a quantitative abstraction-refinement framework to automate the process of constructing abstractions efficiently. Using state-of-the-art verification technologies such as SAT solvers and symbolic model checking, we have implemented a verifier for ANSI-C programs that exhibit probabilistic behaviour and applied it to real networking software.