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

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.

Call for Papers: FM 2024

The Call for Paper for Formal Methods 2024 is announced.

Open researcher positions available

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