KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems

Table of Contents Overview Summary Case Studies Quick Usage

Download or try Online or consult API Doc or study Source

Overview

Self-driving cars, autonomous robots, modern airplanes, or robotic surgery: we increasingly entrust our lives to computers and therefore should strive for nothing but the highest safety standards - mathematical correctness proof. Proofs for such cyber-physical systems can be constructed with the KeYmaera X prover. As a hybrid systems theorem prover, KeYmaera X analyzes the control program and the physical behavior of the controlled system together.

KeYmaera X features a minimal core of just 1700 lines of code that isolates all soundness-critical reasoning. Such a small and simple prover core makes it much easier to trust verification results. Pre-defined and custom tactics built on top of the core drive automated proof search. KeYmaera X comes with a web-based front-end that provides a clean interface for both interactive and automated proving, highlighting the most crucial parts of a verification activity.

• Download KeYmaera X to use it on your computer
• Try KeYmaera X Online for first impressions (but reduced speed)

Summary

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 is built up from a small trusted core. The core contains a finite list of locally sound dL axioms that are instantiated using a uniform substitution proof rule. Isolating all soundness-critical reasoning in this axiomatic core obviates the otherwise intractable task of ensuring that proof search algorithms are implemented correctly. This enables advanced proof search features---such as aggressive, speculative proof search and user-defined tactics built using a flexible tactic language---without correctness concerns that could undermine the usefulness of automated analysis. Early experimentation with KeYmaera X suggests that a single layer of tactics on top of the axiomatic core provides a rich language for implementing novel and highly sophisticated automatic proof procedures.

Case Studies

These are a few of the many other case studies that have been verified in KeYmaera X:

More case studies are also reported in corresponding publications.

Quick Usage

Also get quick usage help any time with the  ?  menu button in KeYmaera X.

Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of any sponsoring institution.