Design defects in embedded systems can be elusive and expensive. Verification research aims to provide algorithms that automate the process of finding design bugs and in special cases even prove correctness. In this talk, I will present two recent developments in this area from our research: (1) a framework for verification of progress properties and (2) an approach for proving properties from simulations or dynamic data. The first builds on a connection between termination analysis of programs and control theory. It provides algorithms for automatic stability verification for rectangular hybrid models. Augmented with Lyapunov functions these algorithms can handle nonlinear hybrid models as well. The second approach combines static analysis of the system model with dynamically generated data (e.g. simulations or logs) for bounded verification of nonlinear and distributed systems of medium dimensions.
Sayan Mitra is an Assistant Professor of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign. His research aims to develop mathematical, algorithmic and software tools for design and analysis of distributed and cyber-physical systems. Sayan graduated from MIT in 2007 and spent one year as a post-doctoral researcher at the Center for Mathematics of Information of CalTech. His research group has received several awards; most recently, the National Science Foundation's CAREER award in 2011, AFOSR Young Investigator Research Program Award in 2012, Best paper award at FORTE/FMOODS 2012, Samsung GRO Award 2012.