AI-based components have become integral to Cyber-Physical Systems (CPS), enabling transformative functionalities across various domains including transportation, energy, and medicine. Specifically, machine learning components are now widely used for perception, control, and decision-making in safety-critical applications, necessitating rigorous verification methods to ensure safe deployment in real-world environments.

In this talk, we present a formal approach for verifying the safety of AI-enabled CPS. We focus on closed-loop systems that integrate dynamical models of physical processes with neural network-based perception and control modules. We explore two verification scenarios: (1) controllers implemented as neural networks, and (2) perception pipelines combining camera models with neural networks. A key challenge in both settings is the scalability of verification algorithms, particularly due to the large size of neural networks and the complexity introduced by image-based perception.

To address these challenges, we propose abstraction techniques that simplify system representations and make verification tractable. Specifically, we introduce two novel data structures: Interval Neural Networks, which provide abstract representations of neural network behaviors, and Interval Images, which serve as abstract symbolic representations of a set of images. We also present novel abstraction-refinement algorithms that efficiently search for small abstractions to prove system safety. Our experimental results demonstrate that these abstraction-refinement algorithms significantly improve scalability and efficiency by quickly identifying small abstractions to prove safety, enabling the analysis of complex, large-scale AI-enabled CPS.

We also discuss verification approaches for evolving neural networks and highlight ongoing work on stability analysis, refinement checking, compositional analysis, and related challenges.

This work is a collaborative effort with students and postdoctoral researchers in the Trustworthy AI and Autonomous Systems (TRAITS) Lab, in collaboration with the Indian Institute of Science (IISc), and is supported by NSF and Amazon Research Awards.

Pavithra Prabhakar is a Professor of Computer Science at Kansas State University, where she holds the Peggy and Gary Edwards Chair in Engineering. She obtained her doctorate in Computer Science from the University of Illinois at Urbana-Champaign (UIUC) in 2011, from where she also obtained a masters in Applied Mathematics. She was a CMI (Center for Mathematics of Information) fellow at Caltech for the year 2011-12. She has been on the faculty of Kansas State University since 2015, and has previously held a faculty position at the IMDEA Software Institute. Her main research interest is in the Formal Analysis of Cyber-Physical Systems, with emphasis on both theoretical and practical methods for verification and synthesis of hybrid control systems. Her papers have been selected for a best paper honorable mention award from Hybrid Systems: Computation and Control, best papers of MEMOCODE and invited papers at Allerton and American Control Conference. She has been awarded a Sohaib and Sara Abbasi fellowship from UIUC, an M.N.S Swamy medal from the Indian Institute of Science for the best masters thesis, a Marie Curie Career Integration Grant from the European Union, Michelle Munson-Serban Simu Keystone Research Faculty Scholarship and Dean’s Award for Excellence in Research from the KSU College of Engineering, a summer faculty fellowship from AFRL, an NSF CAREER Award and an ONR Young Investigator Award.