KeYmaera X: Documentation

Table of Contents Documentation Using KeYmaera X User Tutorial First-time Setup Models Proofs Tactics Tool Architecture Publications

⇓ Download ⇓ or get Source and read Book and watch Videos and follow Tutorial

Documentation

KeYmaera X Tutorial Textbook: Logical Foundations of Cyber-Physical Systems. Springer, 2018. Video lectures: Logical Foundations of Cyber-Physical Systems Wiki for KeYmaera X Grammar for KeYmaera X ScalaDoc API Documentation for KeYmaera X Bellerophon tactics language Tactics library Additional information: Mailing list for KeYmaera X FM 2016 tutorial Tactics and Proofs for Cyber-Physical Systems at FM'16 [slides] Invited talk Logic & proofs for cyber-physical systems at IJCAR'16' [slides] Invited tutorial Proving Hybrid Systems at FMCAD'15 Invited tutorial Logic of dynamical systems at LICS'12 with slides and extended version How to Model and Prove Hybrid Systems with KeYmaera: A Tutorial on Safety. STTT 2016 STTT'16 KeYmaera X feature request & bug tracker Source code (open source under GPL) CPSWEEK 2016 tutorial From Idea to Provably Safe Implementation: Modeling, Proving, Simulation, and Synthesis in KeYmaera X at CPSWEEK'16 [slides]

Cheat Sheet or Textbook or Videos or Tutorial or User Videos or API Doc or Wiki or FM tutorial or LICS tutorial or LICS slides or STTT tutorial

Using KeYmaera X

After starting KeYmaera X and signing in, usage information can be obtained from the Help menu on the top right. You also always have the button  ?  for quick help.

• Quick usage help: display help with the  ?  menu button on each page.

User Tutorial

KeYmaera X Tutorial

1. Usage Overview Video
2. KeYmaera X Tutorial

First-time Setup

1. Start the KeYmaera X Prover, which will open its user interface in your web browser.
2. Configure your arithmetic solver from the menu KeYmaera X→Preferences and choose Save. The support for Mathematica and Wolfram Engine provide significantly more functionality than that of Z3 which ships with KeYmaera X.
3. To get started you may want to import the textbook examples by going to menu KeYmaera X→Models and then select Import for the LFCPS 2018 Textbook or LFCPS Tutorial collection.

Models

KeYmaera X→Models menu entry displays your CPS models. Import models from tutorials or load your own models with KeYmaera X→New Model. Choose an action to show or start proofs for a specific model, generate monitors, code, or test cases. As a simple example, remember the bouncing ball from your childhood days.

[KeYmaera X Model]

Proofs

KeYmaera X→Proofs menu entry displays all CPS proofs that you've completed or started. Choose an action to open or export a proof. You can start a new proof by selecting the action Start Proof on your favorite model listed from the KeYmaera X→Proofs menu entry.

Tactics

Tactics are used extensively in the implementation of KeYmaera X. They are also useful to customize proof search for a model. One way to learn how KeYmaera X tactics work is to observe how KeYmaera X automatically generates a tactic for you as you interact with a proof. Select the Tactic tab at any time while proving a model to see what tactic program would have performed the same proof you just did per hand.

Several of the tutorial examples also come with a range of different styles of tactics that prove them.

1. Click KeYmaera X→Models menu entry.
2. Click on Browse in the tactics column for one of the models.
3. Click Prove associated model.

These examples are also provable directly with much simpler tactics or fully automatically. But the custom tactics demonstrate different features and give a good idea on the structure of the resulting proof.

The tactics language Bellerophon and its tactic library is also described in the ScalaDoc API.

Tool Architecture

KeYmaera X was designed to achieve powerful automation of hybrid systems theorem proving while ensuring soundness. The architecture of KeYmaera X is separated into a small, soundness-critical microkernel and an extensive tactic framework to regain and exceed the convenience of powerful proof rules from the small soundness-critical basis of a prover microkernel. KeYmaera X is powered by multidynamics technology.

Publications

For more detail, see List of KeYmaera X Publications.

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.