A cyber physical system is a system that features a tight coordination between its computational and physical components. They arise frequently in many application domains, including aviation, automotive, railway, and robotics. Because these systems operate in the physical world, stringent safety requirements are usually imposed on cyber-physical system designs. Hybrid systems model cyber-physical systems as dynamical systems with interacting discrete transitions (tipically the computational component) and continuous evolutions (typically the physical component). Historicaly, automatic verification is well developed for guaranteeing correct functioning of discrete systems (like computer programs) using logic and formal verification techniques, but what to do about hybrid systems? How can we ensure that cyber-physical systems are guaranteed to meet their design goals, e.g., that an aircraft following all protocols cannot crash into another one? This talk describes how logic and formal verification can be lifted to hybrid systems. It presents the theoretical and practical foundations of logical analysis of hybrid systems. The talk describes a logic for hybrid systems called differential dynamic logic and gives a compositional proof technique, complete relative to a first order theory for differential equations. This approach is implemented in the verification tool KeYmaera and has been used successfully for verifying nontrivial properties of aircraft, railway, and car control applications. The logical approach is also interesting from a theoretical perspective, because it shows how verification techniques for continuous dynamics can be lifted completely to hybrid systems. Work by André Platzer.