摘要：Modern embedded systems involve interactions between computation, communication, and control. Examples of such systems include air-traffic control systems, robotics, autonomous vehicles, and medical devices among others. Design defects in such systems can be difficult to catch and expensive to fix. Formal verification aims to address this problem by providing algorithms that automate the process of finding design bugs; in special cases these algorithms can also provide correctness guarantees. In this talk, I will present recent results on automatic verification of inevitability and bounded safety. The inevitability verification algorithm iteratively abstracts and refines the discrete-continuous (or hybrid) behavior of the embedded system and its complete for rectangular initialized hybrid automata. The trace-based verification algorithm uses simulation data for constructing bounded time reach sets. I will discuss experimental results which suggest that the algorithm can scale to systems with 10 continuous state variables and many discrete states. In the process, we will encounter several techniques from program analysis and control theory.

 

演讲人简历：Sayan Mitra is an Assistant Professor of Electrical and Computer Engineering and Affiliate Assistant Professor of Computer Science at the University of Illinois at Urbana-Champaign. His research interests are in formal verification, distributed algorithms, and formal methods. Prior to joining Illinois, he was a post-doctoral fellow at the Center for Mathematics of Information of California Institute of Technology for a year and earned a Ph.D. from MIT in 2007. He obtained a MS in Computer Science from Indian Institute of Science, Bangalore and a Bachelors degree in Electrical Engineering from Jadavpur University, Calcutta. He received National Science Foundation's CAREER award in 2011, Air Force's Summer Faculty Fellowship award in 2011, and Air Force Office of Scientific Research Young Investigator Award in 2012.