Ensuring the safety of dynamical systems in complex and uncertain environments is challenging. A mathematically rigorous way to ensure safety is to first create a formal model of the system and then to compute the states that are reachable in this model. Provided that the model is conservative, a safe model implies that the true system is also safe. In this talk, we give an overview of a state-of-the art technique for such a reachability analysis. We discuss some of the challenges and illustrate some applications in recent case studies.