Verification and Synthesis Algorithms for Safe Autonomy

A single design defect can wreak havoc across thousands of deployed instances of autonomous systems or cyber-physical systems (CPS) such as self-driving cars, drones, and medical devices. Can rigorous approaches based on formal methods and control theory improve safety in autonomous systems by transforming the conventional trial-and-error paradigm? Verification and synthesis for typical models of real-world autonomous systems and CPS are well-known to be theoretically undecidable, and approximate solutions are challenging due to their high dimensionality, nonlinearities, and their nondeterministic and hybrid nature. In this talk, I will present new verification and synthesis algorithms which suggest that these challenges can be overcome and that rigorous approaches are indeed promising. The common ingredient underlying my algorithms is automated sensitivity analysis, which leads to semi-decision procedures for verification and synthesis, with soundness, completeness, and optimality guarantees. I will introduce the first bounded safety verification algorithm for nonlinear hybrid systems. This data-driven algorithm, which is the basis for the C2E2 tool, can also be used for compositional verification of networked and distributed autonomous systems. Then I will present my work on the DryVR framework, which is the first approach that can verify real-world CPS with incomplete or imprecise mathematical models. The final part of my talk will rely on symbolic sensitivity analysis with applications in control synthesis for large linear systems with disturbances. I will discuss successful applications in autonomous driving scenarios, powertrain control, circuits, and medical devices as examples to show the power of these tools for solving challenging problems in a wide range of engineering domains.