Model checking is a powerful verification technique for bug hunting in
hardware circuits and software programs. Its extension to probabilistic
models enables the quantitative evaluation of system performance and
reliability along with correctness. Probabilistic model checking has
applications in e.g. robotics, energy-aware computing, RAMS analysis,
distributed computing, and probabilistic programming. It provides hard
guarantees that quantitative system requirements are met, facilitates
bottleneck analysis, and recently enables synthesizing optimal system
parameters. In this talk, I present some applications, uncover some of
its key algorithmic ingredients, show its scalability to Markov models
of millions of states, and give some insights in recent developments in
parameter synthesis.