KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems

Table of Contents
  1. Quickly
  2. Announcements
  3. Overview
  4. Summary
  5. Case Studies
  6. Quick Usage
⇓ Download or get
Source or read
Book or watch
Videos

Quickly

 ⇓ Download ⇓     KeYmaera X    Installation Info 

Announcements

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 and hybrid games 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.

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 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.

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. KeYmaera X demonstrates that tactics on top of the axiomatic core provide 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:

Other case studies are reported in corresponding publications.

Quick Usage

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

Initial conjecture is loaded
Extract assumptions
Split compound assumptions into single facts
Prove loops with induction
Get proof suggestions
Work on subproblems in context
Proved!

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.