Carnegie Mellon University
Hybrid systems model cyber-physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. They arise frequently in many safety-critical application domains, including aviation, automotive, railway, and robotics. But how can we ensure that these systems are guaranteed to meet their design goals, e.g., that an aircraft will not crash into another one?
This talk describes how logic and formal verification can be lifted to hybrid systems. It presents the theoretical and practical foundations of logical analysis of hybrid systems. The talk describes a logic for hybrid systems called differential dynamic logic and surveys a perfectly compositional proof technique. This logical approach is implemented in the verification tool KeYmaera and has been used used successfully for verifying nontrivial properties of aircraft, railway, and car control applications. The logical approach also shows how verification techniques for continuous dynamics can be lifted to hybrid systems by a complete axiomatization.
André Platzer is an Assistant Professor in the Computer Science Department at Carnegie Mellon University. His interests include verification of cyber-physical systems, logic in computer science, automated theorem proving, and model checking. He received an ACM Doctoral Dissertation Honorable Mention Award, an NSF CAREER Award, the Best Paper Awards at TABLEAUX'07 and at FM'09. André Platzer was also named one of the Brilliant 10 Young Scientists by the Popular Science magazine 2009 and one of the AI's 10 to Watch 2010 by the IEEE Intelligent Systems Magazine.