Abstract. Probability features increasingly often in software and hardware systems: it is used in distributed co-ordination and routing problems, to model fault-tolerance and performance, and to provide adaptive resource management strategies. Probabilistic model checking is an automatic procedure for establishing if a desired property holds in a probabilistic model, aimed at verifying probabilistic specifications such as "leader election is eventually resolved with probability 1", "the chance of shutdown occurring is at most 0.01%", and "the probability that a message will be delivered within 30ms is at least 0.75". A probabilistic model checker calculates the probability of a given temporal logic property being satisfied, as opposed to validity. In contrast to conventional model checkers, which rely on reachability analysis of the underlying transition system graph, probabilistic model checking additionally involves numerical solutions of linear equations and linear programming problems. These lecture notes summarise both the theory and the practical details of automatic verification of probabilistic systems against temporal logic specifications. We cover discrete- and continuous-time Markov chains, Markov decision processes and probabilistic timed automata, as well as the temporal logics PCTL, CSL and PTCTL. The usefulness of the techniques is demonstrated through a number of case studies analysing real-world probabilistic protocols performed with PRISM, a probabilistic model checker developed at the University of Birmingham.