Colloquium Details
Verification and Synthesis Algorithms for Safe Autonomy
Speaker: Chuchu Fan, University of Illinois at Urbana-Champaign
Location: 60 Fifth Avenue 150
Date: March 6, 2019, 2 p.m.
Host: Subhash Khot
Synopsis:
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 hard 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.
Speaker Bio:
Chuchu Fan is a Ph.D. candidate in the Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign. She received her Bachelor's degree from Tsinghua University, Department of Automation in 2013. Her research interests are in the areas of formal methods and control for safe autonomy. She is a recipient of multiple prestigious awards including Mavis Future Faculty Fellowship (2018), Young Researcher for Heidelberg Laureate Forum (2017), Rising Stars in EECS (2016), EMSOFT'16 Best Paper finalist, and Robert Bosch Best Verification Award in CPSWeek'15. Her research achievements are also recognized with a Mac Van Valkenburg Research Award (2018), a Yi-Min Wang and Pi-Yu Chung Endowed Research Award (2017), and a Rambus Fellowship (2016).
Notes:
In-person attendance only available to those with active NYU ID cards.