Fri 11/19/2010, 2:00 PM, GHC-6501
AbstractThe widespread deployment of computing devices that manage and control physical processes in safety critical environments, has made their analysis and verification a very important problem. Since formal models that disregard the physical processes tend to be conservative and suboptimal, the most popular way to model and analyze such systems is using hybrid systems, that have finitely many control states to model discrete behavior and finitely many real valued variables that evolve continuously with time to model the interaction with the physical world. Despite considerable progress in the last couple of decades, the automated verification of cyber physical systems remains stubbornly challenging. In this talk we will discuss one approach to making the analysis more scalable, namely, by automatically constructing "simpler", "smaller" models, and then analyzing these approximated models. We will present a couple of techniques to approximate hybrid models, based on the Stone-Weierstrauss Theorem and counter-example guided abstraction-refinement (CEGAR), and discuss their applications to automated verification.
BiographyMahesh Viswanathan obtained his bachelor's degree in computer science from the Indian Institute of Technology at Kanpur in 1995, and his doctorate from the University of Pennsylvania in 2000. He was a post-doctoral fellow at DIMACS with a joint appointment with Telcordia Technologies in 2000-01. Since 2001, he has been on the faculty at the University of Illinois at Urbana-Champaign. His research interests are in the core areas of logic, automata theory, and algorithm design, with applications to the algorithmic verification of systems.