It is our pleasure to announce that our Keynote speaker on HSCC’24 will be Prof. Sayan Mitra from UIUC.
Sayan Mitra is a Professor of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign (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 tools. Sayan received his PhD from MIT, MS from Indian Institute of Science, and an 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 contributions have been recognized with ACM Doctoral Dissertation Award, NSF CAREER Award, AFOSR YIP, and several best paper awards.
Data-driven Verification for Safe Autonomy: Reachability, Entropy, and Perception Contracts
Abstract: Ensuring the trust and safety of autonomous systems demands an expansion of formal methodologies to accommodate a broader array of models and assumptions. In the first part of this talk, I will discuss methods of assessing system safety through reachability analysis and how different model assumptions impact their effectiveness. These methods combine simulation data with sensitivity analysis for answering questions about system safety. At one end, complete dynamical models offer strong assurances, but their utility can be limited. Allowing probabilistic notions of sensitivity, we get algorithms capable of addressing real-world scenarios. This flexible approach informs our current work on the Verse framework which aims to make code-level analysis for autonomous multi-agent scenarios accessible to undergraduates. In the second part, I will discuss a safety analysis method for learning-enabled autonomous systems using abstraction and substitutivity. Specifically, this derives the conditions when a hypothetical ideal observer can be substituted with a practical observer implemented by a machine learning model. This leads to the notion of a perception contract which approximates the machine learning model and it can substitute a perfect observer while preserving the safety proof. We will discuss applications of this method in the analysis for vision-based lane keeping and automated landing systems.