CSL PhD Thesis Award 2020: "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, control theory, and machine learning improve safety in autonomous systems by transforming the conventional trial-and-error paradigm? Providing safety guarantees for typical models of real-world autonomous systems and CPS are well-known
to be hard due to their high dimensionality, non-linearities, nondeterminism, and model inaccuracies. In this talk, CSL PhD Thesis Award Winner Prof. Chuchu Fan presents her work on verification and synthesis algorithms that suggest that these challenges can be overcome and that rigorous approaches are indeed promising. She also discusses the tools she developed and successful applications in autonomous driving scenarios, powertrain control, robot motion planning, circuits, and medical devices as examples to show the power of these tools for solving challenging problems in a wide range of engineering domains. Towards the end of the talk, she introduces her recent work on using machine learning techniques to extend these rigorous approaches to certify learning-enabled autonomous systems.