Research Areas of André Platzer

KeYmaera: A Hybrid Theorem Prover for Hybrid SystemsLogical Analysis of Hybrid Systems
Logic for Distributed Hybrid SystemsLogical Foundations of Cyber-Physical Systems
Logic for Stochastic Hybrid Systems15-424: Foundations of Cyber-Physical Systems (Fa'13)
Case Study: European Train Control SystemCase Study: Formal Verification of Curved Flight Collision Avoidance Maneuvers

Overview

Table of Contents
  1. Hybrid System Cyber-Physical Systems Verification
  2. Logic-based Verification
  3. KeYmaera: A Hybrid Theorem Prover for Hybrid Systems

From this page, you will find some of my research topics, mainly in the area of logic in computer science and mathematics, especially logical foundations of cyber-physical systems, including verification of hybrid systems, programs, and differential dynamic logic for hybrid programs. Additionally, this site hosts some of my publications.

Further information on research topics that are closely associated with tools implementing these approaches is presented in the Tools section.

Implementations of some of these algorithms are contained in the Tools section.

Research

My primary research interests are in the field of verification of complex systems, especially hybrid systems with nontrivial interacting discrete and continuous dynamics. I am particularly interested in designing and analyzing verification techniques and verification logics, and in using these to develop automatic verification tools that help producing reliable complex systems, e.g., in aeronautical, railway, automotive, robotic, or biomedical applications.

Below are short descriptions of some research topics and directions that I think are particularly exciting.

Hybrid System 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 (also known as cyber-physical 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. Discrete dynamics primarily results from the logical decision-making in digital controllers, embedded systems, or full-blown computer systems.

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 an enormous 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 the goal of my research.

Logic-based Verification

As an emerging development in hybrid systems, rigorous symbolic methods have been developed recently, which 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 logics that are suitable for the mixed discrete-continuous realm of hybrid systems, in which properties of their transitions can be stated and proven. See differential dynamic logic for hybrid systems.

One of my primary research ambitions is to develop the theory, practice, and applications of logic-based verification approaches for hybrid systems.

Also see this overview of logics for dynamical systems.

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 and air traffic management.