SHF: Small: Scalable Formal Verification of ANN controlled Cyber-Physical Systems

Artificial Neural Networks (ANN) are increasingly being employed to monitor and control Cyber-Physical Systems (CPS), as in autonomous ground and aerial vehicles. With increasing complexity and safety criticality of these systems, formal-verification techniques that provide rigorous guarantees are urgently needed. The broad goal of the research is to develop novel algorithms and software tools for formal verification of ANN-controlled CPS (ANN-CPS). One of the main challenges of existing techniques is their scalability to large number of neurons and complex physical dynamics. Using the novel concept of Interval Neural Networks, coupled with ideas from formal methods such as counter-example guided abstraction refinement and approximate bisimulation, the project investigates scalable formal verification techniques for ANN-CPS. The results of the project will enable rigorous analysis of complex ANN-CPS possible, thereby enhancing their reliability in applications such as autonomous driving. Further, the PI is engaged in course development, mentorship of undergraduate and graduate students, and outreach activities for K-12 students, with the broader aim of motivating and building the workforce for formal analysis of cyber-physical systems. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria. NSF Award ID: 2621137 | Program: 01002021DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Pavithra Prabhakar | Institution: University of New Mexico, ALBUQUERQUE, NM | Award Amount: $105,455 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2621137 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2621137.html