We present a methodology and implementation for verifyingANSI-C programs that exhibit probabilistic behaviour, such as failures orrandomisation. We use abstraction-refinement techniques that representprobabilistic programs as Markov decision processes and their abstrac-tions as stochastic two-player games. Our techniques target quantitativeproperties of software such as "the maximum probability of file-transferfailure" or "the minimum expected number of loop iterations" and theabstractions we construct yield lower and upper bounds on these prop-erties, which then guide the refinement process. We build upon state-of-the-art techniques and tools, using SAT-based predicate abstraction,symbolic implementations of probabilistic model checking and compo-nents from GOTO-CC, SATABS and PRISM. Experimental results showthat our approach performs very well in practice, successfully verifyingactual networking software whose complexity is significantly beyond thescope of existing probabilistic verification tools.
展开▼
