Carnegie Mellon University Pittsburgh United States
Cyber-physical systems CPS ranging from critical infrastructures such as power plants, to modern semi autonomous vehicles are systems that use software to control physical processes that interact in intricate manners. This makes verification of the software complex and unwieldy. In this report, an approach towards taming part of the complexity is described. The approach utilizes intrinsic multi-modal redundancies to detect brewing problems, provides formal guarantees for control algorithms, and automates the software production to implement these algorithmic ideas with guarantees about the correctness of the resulting implementations.