Title: Data-driven Verification for Safe Autonomy: Reachability, Entropy, and Perception Contracts
Abstract
Todays verification technologies for autonomous and cyber-physical systems require detailed models which is one of the barriers that keep them from being widely used. In this talk, I will first present the basic idea of data-driven reachability analysis for systems with both black and white-box components. This line of research has culminated in the Verse framework which supports code-level analysis of autonomous multi-agent scenarios, and which has been used for realistic systems as well as in the classroom. Next, I will discuss an interesting connection between verification and a fundamental quantity called topological entropy that quantifies the growth of uncertainty in dynamical systems. Finally, I will discuss a method for assuring end-to-end safety of learning-enabled autonomous systems using perception contracts. The method is based on constructing approximations of perception pipelines, using system-level safety requirements and reachability analysis. We will discuss recent applications of this framework in creating intelligible contracts and end-to-end safety certificates for vision-based lane keeping, automated landing, and in formation control.
Speaker Bio
Sayan Mitra is a Professor and Associate Head of Grad Affairs of the Department of Electrical and Computer Engineering at UIUC. His research interests are in formal verification, autonomous systems, and control theory. His group’s research has led to the creation of several verification and synthesis software tools which are in different stages of commercialization. Sayan received his PhD from, MS from Indian Institute of Science and undergraduate degree in Electrical Engineering from Jadavpur University. His textbook on verification of cyber-physical systems was published in 2021 (MIT press). His group’s work has been recognized with ACM Doctoral Dissertation Award, NSF CAREER Award, AFOSR YIP, and several best paper awards.
