The project addresses the verification of system dependability properties. We quantify properties such as the worst-case risk of reaching an unsafe state within a given time or cost bound. The technical focus is on extending and improving stochastic model checking methods to support a broad range of discrete-time and continuous-time stochastic models. Special emphasis is put on the verification of parametric systems, making it possible to evaluate and optimize energy-aware, self-stabilizing systems.