Having scalable verification and control tools is crucial for the safe operation of highly dynamic systems such as complex robots. Yet, most current tools rely on either convex optimization, which enjoys formal guarantees but struggles scalability-wise, or blackbox learning, which has the opposite characteristics. We will present a new method that improves the scalability of sum-of-squares programming-based system verification by ~3x (e.g., to verify a 32 states robot); in addition, the method computes tighter results 2-3 orders of magnitude faster. We will also introduce one of the first verification frameworks for partially observable systems modeled or controlled by LSTM-type (long short term memory) recurrent neural networks.

Bio: Shen Shen is a postdoctoral research associate and lecturer at ORFE, Princeton University. Shen received her B.S. in Aeronautics and Astronautics and B.A. in English Literature from the Harbin Institute of Technology, China, and her S.M. and Ph.D. in in Electrical Engineering and Computer Science (with concentrations in educational psychology and robotics respectively) from MIT.