Event Location: NSH 1305
Bio: André Platzer is an Assistant Professor in the Computer Science Department at Carnegie Mellon. Dr. Platzer developed the theory, practice, and applications of logical analysis and verification of hybrid systems, and he proved the very first completeness theorem for hybrid systems. He introduced compositional verification techniques and methods that can verify hybrid systems without solving their differential equations (called differential invariants). In addition, he led the development of the first theorem prover for hybrid systems (KeYmaera) and he has worked on verification of aircraft, railway, and car control systems.

In recent work, André Platzer has introduced the first formal verification approach for distributed hybrid systems, in which participants can appear and disappear dynamically while the system follows its hybrid dynamics.

Abstract: Hybrid systems model cyber-physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. They arise frequently in many application domains, including aviation, automotive, railway, and robotics. Because these systems operate in the physical world, stringent safety requirements are usually imposed on cyber-physical system designs. There is a well-understood theory for guaranteeing correct functioning of computer programs using logic and formal verification techniques. But what about cyber-physical systems? How can we ensure that cyber-physical systems are guaranteed to meet their design goals, e.g., that an aircraft cannot 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 gives a perfectly compositional proof technique. This logical approach is implemented in the verification tool KeYmaera and has been used successfully for verifying nontrivial properties of aircraft, railway, and car control applications. The logical approach is also interesting from a theoretical perspective, because it shows how verification techniques for continuous dynamics can be lifted completely to hybrid systems.