Distinguished Turing Lecture Series
Delta-reachability Analysis for Hybrid Systems
Sep. 25, 2015 @ 02:00 pm
Florida International University
Professor Ed Clarke
Carnegie Mellon University
School of Computing and Information Sciences
We present the framework of delta-complete analysis for bounded reachability problems of hybrid systems. It encodes the reachability problems of hybrid systems to first-order formulas over the real numbers, which are solved by delta-decision procedures. The key idea is to check an over approximation of the reachability problem which can demonstrate robustness of a hybrid system. The analysis strengthens the verification because robustness implies safety. In contrast to the undecidability result of the general reachability problem for nonlinear hybrid systems, the delta-reachability problem is decidable and has a reasonable complexity bound (PSPACE-complete). Our implementation of the techniques, an open-source tool dReach, shows that it can handle several highly nonlinear hybrid system models that arise in biomedical and robotics applications.
Edmund M. Clarke is the FORE Systems University Professor of Computer Science at Carnegie Mellon University. He received his Ph.D. from Cornell University and taught at Duke and Harvard Universities before joining CMU in 1982. His research interests include hardware and software verification and automatic theorem proving. In particular, his research group developed Symbolic Model Checking using BDDs, Bounded Model Checking using fast CNF satisfiability solvers, and pioneered the use of Counter Example-Guided-Abstraction-Refinement (CEGAR). He is a co-founder of the conference on Computer Aided Verification (CAV). He has received numerous awards for his contributions to formal verification of hardware and software correctness, including the IEEE Goode Award, the ACM Kanellakis Award, the ACM Turing Award, and the CADE Herbrand Award. Dr. Clarke is a member of the National Academy of Engineering and the American Academy of Arts and Sciences. Most recently he received the 2014 Franklin Institute Bower Award and Prize for Achievement in Science for verification of computer systems.