Logic of Autonomous Dynamical Systems

KeYmaera X

KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics. Reasoning about complicated hybrid systems requires support for … sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute tactics in parallel, and interface with partial proofs via an extensible user interface. KeYmaera X also is a verification tool for differential game logic (dGL), a logic for specifying and verifying properties of hybrid games with mixed discrete, continuous and adversarial dynamics. — keymaerax.org

Differential Dynamic Logic

Differential dynamic logic (dL) is a logic for specifying and verifying hybrid systems combining discrete and continuous dynamical systems. Such hybrid systems combine discrete dynamics, e.g., for representing the instantaneous change of computer … decisions with continuous dynamics represented as differential equations, e.g., for the continuous motion of a car or aircraft. The purpose of dL is that this logic can be used to describe/specify and prove/verify correctness properties for hybrid systems given operationally as hybrid programs using the dL proof calculus. The logic dL and its proof calculus are the basis of the deductive verification tool KeYmaera for hybrid systems and its successor KeYmaera X. In addition, the hybrid systems and correctness properties formulated in dL may include symbolic parameters, which can be free or quantified to discover the required parametric safety constraints. — keymaerax.org

Logical Foundations of CPS

Cyber-physical systems (CPSs) combine cyber capabilities, such as computation or communication, with physical capabilities, such as motion or other physical processes. Cars, aircraft, and robots are prime examples, because they move physically in … space in a way that is determined by discrete computerized control algorithms. Designing these algorithms is challenging due to their tight coupling with physical behavior, while it is vital that these algorithms be correct because we rely on them for safety-critical tasks. — Website

Complete Dynamic Logic of Communicating Hybrid Programs

Communicating hybrid programs (CHPs) are a programming language for modeling parallel interactions of cyber-physical systems, e.g. multiple trains, aircraft, or robots. The dynamic logic of communicating hybrid programs (dLCHP) allows to study the … safety of such parallel interactions. Its highlight is a modular proof calculus that identifies all essential principles underlying parallel cyber-physical systems as simple and modular axioms—yet is proven to be complete! Accepted at Journal of Automated Reasoning (JAR). — Paper

Semi-competitive differential game logic

Semi-competitive differential game logic (dGLsc) is a logic for verifying two-player non-zero sum games where both players have an individual goal. The players behave semi-competitively, i.e. they help each other where possible and compete where … necessary. Thus, dGLsc addresses the challenge that even though each player may benefit from knowledge of the other player’s goals, e.g., concerning shared safety objectives, unsafety might still arise if every player were to mutually assume the other player would act to avoid unsafety. The logic is therefore particularly well suited to verify, for example aerial collision avoidance with the dGLsc proof calculus. — Paper

Three Papers Accepted at IJCAR 2026

Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements, Enguerrand Prebet, André Platzer

Complete Robust Hybrid Systems Reachability, Noah Abou El Wafa, André Platzer

A Deductive Refinement-Calculus for Differential-Algebraic Programs Jonathan Hellwig, Long Qian, André Platzer

Open researcher positions available

The group has open positions for PhD students, doctoral, and postdoc researchers.

Adaptive Shielding via Parametric Safety Proofs

How can we keep cyber-physical systems safe in unknown, changing environments? Our latest work empowers engineers to build safety monitors that become increasingly permissive as knowledge about the world is gathered at runtime. Such monitors can be automatically extracted from parametric safety proofs verified with KeYmaera X, leveraging minimal amounts of expert knowledge to offer an unprecedented combination of rigor, modelling flexibility and runtime efficiency.