|⇓ Download ⇓
Online or get
Source and read
Book and watch
Videos and follow
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.
- Start the KeYmaera X Prover, which will open its user interface in your web browser.
- 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.
- 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 collection.
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]
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 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.
- Click KeYmaera X→Models menu entry.
- Click on Browse in the tactics column for one of the models.
- Click Prove associated model.
Tool ArchitectureKeYmaera 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 kernel and an extensive tactic framework to regain and exceed the convenience of powerful proof rules.
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.