Download KeYmaera Verification Tool for Hybrid Systems

Table of Contents
  1. Download KeYmaera Installer
  2. Webstart KeYmaera
  3. KeYmaera Extras
  4. Support
  5. Developers
  6. Older Versions: KeYmaera 1.5-3.2
Download or
WebstartKeYmaera
Logical Analysis of Hybrid Systems

Download KeYmaera Installer

The preferred way of running KeYmaera is to run its KeYmaera Installer. The KeYmaera Installer will download and install KeYmaera locally on your computer and make sure your local copy of KeYmaera stays up to date.

Requirements and Add-ons:

Once KeYmaera is up and running you can look at examples to get started, for instance:

  1. File->Load Project
  2. Choose Simple Acceleration example
  3. Click Proof->Start to start the automatic prover
For more examples, look at:
  1. File->Load Project
  2. File->Start Tutorial

Webstart KeYmaera

If you are experiencing trouble with the KeYmaera installer, run the KeYmaera Webstart. Java Webstarts need appropriate browser permissions, so the KeYmaera installer is generally easier to work with.

Requirements and Add-ons: Note: For Mac OS X, Java WebStart no longer work in Safari. Use another browser like FireFox or Chrome. You may also have to enable:

If you are having difficulties running the Java WebStart version of KeYmaera, try running from command line

javaws http://symbolaris.com/info/KeYmaera.jnlp
You can also use the KeYmaera Launcher version instead.

Once KeYmaera is up and running you can look at examples to get started, for instance:

  1. File->Load Project
  2. Choose Simple Acceleration example
  3. Click Proof->Start to start the automatic prover
For more examples, look at:
  1. File->Load Project
  2. File->Start Tutorial

KeYmaera Extras

KeYmaera is distributed under the GNU General Public License.

Requirements and Add-ons:

Support

Developers

KeYmaera has been developed in the group of Prof. André Platzer at Carnegie Mellon University and of Prof. Ernst-Rüdiger Olderog at the University of Oldenburg. The basis of KeYmaera is the system KeY, developed jointly in the groups of Prof. Peter Schmitt at the University of Karlsruhe, Prof. Reiner Hähnle at the Chalmers University of Technology in Gothenburg (now TU Darmstadt), and Prof. Bernhard Beckert at the University of Koblenz. The main KeYmaera developers are: With very helpful contributions from:

Older Versions: KeYmaera 1.5-3.2

Older versions of KeYmaera are of archival interest only.

To run the older release KeYmaera 3.2 use the KeYmaera 3.2 Webstart.

To run the older release KeYmaera 3.1 use the KeYmaera 3.1 Webstart.

To run the older release KeYmaera 3.0 use the KeYmaera 3.0 Webstart.

To run the older release KeYmaera 2.1 use the KeYmaera 2.1 Webstart.

To run the older release KeYmaera 2.0 use the KeYmaera 2.0 Webstart.

To run the older release KeYmaera 1.9 use the KeYmaera 1.9 Webstart.

To run the older release KeYmaera 1.8 use the KeYmaera 1.8 Webstart.

To run the older release KeYmaera 1.5 use the KeYmaera 1.5 Webstart.

When starting, the KeYmaera verification tool will ask you to provide paths to external tools. You do not need to configure all of those external tools! KeYmaera will also work without any external tools but only in a restricted mode. We recommend configuring at least one external tool.
/Applications/Mathematica.app/SystemFiles/Links/JLink/SystemFiles/Libraries/MacOSX-x86
/Applications/Mathematica.app/SystemFiles/Links/JLink/SystemFiles/Libraries/MacOSX-x86-64
/Applications/Mathematica.app/Contents/MacOS/MathKernel
You can configure any number of these tools. For configuring external tools use the menu Options->Tool Paths. Be sure to restart KeYmaera after changing tool path options. After you have configured the tools, you can choose which tools to use in the "Hybrid Strategy" tab.