Abstract. In this paper, we describe some practical applications of probabilistic model checking, a technique for the formal analysis of systems which exhibit stochastic behaviour. We give an overview of a selection of case studies carried out using the probabilistic model checking tool PRISM, demonstrating the wide range of application domains to which these methods are applicable. We also illustrate several benefits of using formal verification techniques to analyse probabilistic systems, including: (i) that they allow a wide range of numerical properties to be computed accurately; and (ii) that they perform a complete and exhaustive analysis enabling, for example, a study of best- and worst-case scenarios.