Seminars & Meetings | Abstracts

Wednesday, March 16, 2011

Sayan Mitra
Department of Electrical Engineering
University of Illinois at Urbana-Champaign

Abstraction refinement for verification of hybrid systems

The hybrid automaton framework is an expressive mathematical formalism for modeling a wide variety of cyber-physical systems. While automatic tools for verifying subclasses of hybrid automata, e.g., rectangular initialized automata are available, general hybrid automata are known to be intractable. As a result, creation of tractable abstractions for hybrid models has received a fair bit of attention. In this talk, I will discuss two recent results in this theme. First, I will discuss a counterexample guided abstraction refinement algorithm for safety verification that relies on rectangular-initialized abstractions. This algorithm has been implemented in a new tool and I will present some of the experimental results. Next, I will present an algorithm for stability verification which relies on slow switching, transition invariants, and approximations for hybrid-steps that combine discrete transitions and continuous flows. I will briefly discuss the completeness of both these algorithms for rectangular initialized automata.



Sayan Mitra is an Assistant Professor of Electrical and Computer Engineering at the University of Illinois at Urbana-Champaign since 2008. His research interests are in verification of cyber-physical systems, distributed algorithms, and application of formal methods in automotive and aerospace. 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. He earned a Ph.D. from MIT in 2007 and received National Science Foundation's Faculty Early Career Development award in 2011.