Andre Platzer
Assistant Professor, Computer Science
www

My primary research interests are in the field of verification of cyber-physical systems and hybrid systems with nontrivial interacting discrete and continuous dynamics. I am particularly interested in designing verification logics, and in using them to develop automatic verification tools that help producing reliable complex cyber-physical systems, e.g., in aeronautical, railway, automotive, robotic, or biomedical applications.
Below are short descriptions of a sample of some research topics and directions that I think are particularly exciting.

Cyber-Physical Systems Verification
Ensuring correct functioning of complex physical systems is among the most challenging and most important problems in computer science. Complex systems in the domain of avionics, railway technology, or automotive industries depend more and more on a successful and reliable, tight integration of computer-control into physical systems. Likewise, automatic digital decision-making is getting increasingly important in biomedical applications like artificial respirators or self-monitoring blood glucose regulation for diabetes patients. As a common feature, all those systems are hybrid systems, i.e., they are governed by interacting discrete and continuous dynamics. The continuous dynamics originates, e.g., from the continuous movement of aircraft in space or more generally from the interaction with the physical world. Discrete dynamics primarily results from the logical decision-making in digital controllers, embedded systems, or full-blown computer controllers.
More generally, cyber-physical systems (CPS) combine cyber capabilities (computer and communication) with physical capabilities (sensing and actuation) to solve problems that no part could solve alone. Unlike pure hybrid systems, CPS may also be distributed or may be stochastic.
Because of the fatal consequences of malfunctions, there are tremendous safety requirements for these systems. Significantly beyond the financial risks of malfunctioning classical software in isolated computer systems, ill-devised coordination of semi-autonomous traffic agents or unreliable biomedical devices are a serious hazard for computer-controlled interactions with the physical environment. To avert potential catastrophes, we need reliable verification techniques for analyzing correctness properties of safety-critical hybrid systems. Developing these techniques is one of the goals of my research.

Logic-based Verification
Rigorous symbolic methods have been developed recently that combine capabilities for handling nontrivial dynamics with crucial soundness properties. One particularly elegant approach is to use the power and precision of symbolic logic to characterize and analyze behavioral properties of actual systems. For this, classical uninterpreted first-order logics are not sufficient, but we need dedicated verification logics that are suitable for the mixed discrete-continuous dynamics of hybrid systems.
One of my primary research ambitions is to develop the theory, practice, and applications of logic-based verification approaches for hybrid systems. This includes the development and study of the family of differential dynamic logics.

KeYmaera: A Hybrid Theorem Prover for Hybrid Systems
KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic (dL), which is a real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control, air traffic control, and car control.