  Cyber-physical systems (CPSs) are important whenever computer technology
interfaces with the physical world as it does in self-driving cars or aircraft
control support systems. Due to their many subtleties, controllers for
cyber-physical systems deserve to be held to the highest correctness standards.
Their correct functioning is crucial, which explains the broad interest in
safety analysis technology for their mathematical models, which are called
hybrid systems because they combine discrete dynamics with continuous dynamics.
Differential dynamic logic (dL) provides logical specification and rigorous
reasoning techniques for hybrid systems. The logic dL is implemented in the
theorem prover KeYmaera X, which has been instrumental in verifying ground
robot controllers, railway systems, and the next-generation airborne collision
avoidance system ACAS X. This chapter provides an informal overview of this
logical approach to CPS safety that is detailed in a recent textbook on Logical
Foundations of Cyber-Physical Systems. It also explains how safety guarantees
obtained in the land of verified models reach the level of CPS execution
unharmed.
