This talk will present reachability analysis as a tool for model checking and controller synthesis for dynamic systems. We will consider the problem of guaranteeing reachability to a given desired subset of the state space while satisfying a safety property defined in terms of state constraints. We allow for nonlinear and hybrid dynamics, and possibly nonconvex state constraints. We use these results to synthesize controllers that ensure safety and reachability properties under bounded model disturbances that vary continuously. The resulting control policy is a set-valued feedback map involving both a selection of continuous inputs and discrete switching commands as a function of system state. We show that new control policies based on machine learning are included in this map, resulting in high performance with guarantees of safety. We discuss real-time implementations of this, and present several examples from multiple aerial vehicle control, human-robot interaction, and multiple player games.