Safety and Dependability will cover techniques for the validation of systems against formal specifications. In a first part, safety specifications (something bad never happens) using the Hoare calculus and safe abstraction are covered. A second part refers to termination (something good eventually happens), exploiting well foundedness. In a third part, Markov chains and decision processes are studied, extending the qualitative safety and termination problems from the first part to qualitative/probabilistic properties, and extending them to a simple probabilistic specification language, PCTL. As part of the module, the ability of formulating (probabilistic) models as Markov chains and decision processes are taught, as well as the use of of-the-shelf tools like PRISM or IscasMC for their analysis.