Formal Verification of Neural Network-Controlled Autonomous Systems

Abstract: Deep Neural Networks (DNNs) are increasingly used to control physical/mechanical systems. Self-• driving cars, drones, and smart cities are just examples of such systems, to name a few. However, regardless of the explosion in the use of DNNs within many cyber-physical systems (CPS) domains, the safety and reliability of these DNN-controlled CPS still need to be investigated. Mathematically based techniques for the specification, development, and verification of software and hardware systems, also known as formal methods, hold the promise to provide appropriate rigorous analysis of the reliability and safety of DN-N controlled CPS. In this talk, I will introduce our tools to verify neural networks against input-output specifications. I will then show how to translate different problems in assured autonomy and certifiable perception into a set of input -output specifications on the neural network controller. Finally, I will extend these results into other domains, including the safe offloading of neural network computations and the fairness of neural network-based decision-making.

Bio: Yasser Shoukry is an Associate Professor in the Department of Electrical l Engineering and Computer Science at the University of California, Irvine, where he leads the Resilient Cyber-Physical Systems Lab. Before joining UCI, he spent two years as an assistant professor at the University of Maryland, College Park. He received his Ph.D. in Electrical Engineering from the University of California, Los Angeles in 201S. Between September 2015 and July 2017, Yasser was a joint postdoctoral researcher at UC Berkeley, UCLA, and UPenn. His current research focuses on designing and implementing resilient, Al-enabled, cyber-physical systems and loT. His work in this domain was recognized by the Early Career Award from the IEEE Technical Committee on Cyber-Physical Systems in 2021, the NSF CAREER Award in 2019, the Best Demo Award from the International Conference on Information Processing in Sensor Networks (IPSN) in 2017, the Best Paper Award from the International Conference on Cyber-Physical Systems (ICCPS) in 2016, and the Distinguished Dissertation Award from UCLA EE department in 2016. In 201S, he led the UCLA/Caltech/CMU team to win the NSF Early Career Investigators (NSF-ECI) research challenge. His team represented the NSF- ECI in the NIST Global Cities Technology Challenge, an initiative designed to advance the deployment of Internet of Things (loT) technologies within a smart city. He is also the recipient of the 2019 George Corcoran Memorial Award from the University of Maryland for his contributions to teaching and educational leadership in CPS and loT.

Host: Prof. Borzoo Bonakdarpour (borzoo@msu.edu) Department of Computer Science and Eng.

(Date Posted: 2023-10-13)