Abstract: Hybrid modeling formalisms are obtained by combining two distinct modeling frameworks: discrete state transition systems, which are commonly used to model computation, and continuous dynamical systems, which are used to model physical systems. Several safety-critical systems are naturally modeled using hybrid formalisms, and hence, it is desirable to develop analysis tools and techniques for hybrid systems. Theoretically, however, verification of even reachability properties for very simple kinds of hybrid systems is undecidable.

This talk presents a methodology for verification of hybrid systems based on constructing discrete finite state abstractions for hybrid systems, which are eventually model-checked against safety properties. The abstraction technique combines qualitative methods for abstracting continuous dynamics with standard predicate abstraction technique for abstracting the discrete behavior of hybrid systems. Automation of this technique relies on a decision procedure for the quantifier-free theory of real closed fields, but in a "failure-tolerant" way.

We shall discuss applications to proving correctness of controllers for automobiles, as well as applications to the emerging field of "Systems Biology" and the new challenges it presents.

Biography: Ashish Tiwari received his B.Tech and Ph.D. degrees in Computer Science from the Indian Institute of Technology, Kanpur and the State University of New York at Stony Brook in 1995 and 2000, respectively. He is currently a member of the formal methods group in the Computer Science Laboratory at SRI International. His research interests are in automated deduction, equational reasoning, decision procedures, hybrid systems, and bioinformatics.