This project's objective is to enable assertion-driven development and debugging of cyber-physical systems (CPS), in which required conditions are formalized as part of the design. In contrast with traditional uses of assertions in software engineering, CPS demand a tight coupling of the cyber with the physical, including in system validation. This project uses mathematical models of key physical attributes to guide creation of assertions, to identify inconsistent or infeasible assertions, and to localize potential causes for CPS failures. The goal is to produce methods and tools that use physical models to guide assertion-based verification of cyber-physical systems. An assertion language is being developed that is founded in mathematical logic while providing the familiarity of commonly used programming languages. This foundation enables new automated debugging techniques for CPS. By leveraging models that encode laws of physics and an automated decision procedure, the techniques being developed help identify causes of CPS failures by distinguishing inconsistent or infeasible physical states from valid ones. This model-based approach incorporates means to assess these physical states using both probabilistic and non-probabilistic measures. Two safety-critical applications guide the research and demonstrate the impact on the development of CPS: coordinated control of autonomous vehicles and monitoring and control of left-ventricular assist devices (LVADs). The focus on these safety-critical applications are motivational for recruiting and educating engineering students who have high expectations for how their lives should be enabled by computing advances. Further, this research advances methods needed to validate safe and effective CPS, promoting the public's confidence in their application to safety-critical systems.