Download KeYmaera Verification Tool for Hybrid Systems

Table of Contents
Webstart KeYmaera Download KeYmaera & Documentation KeYmaera Setup and Configuration Support Developers

Launch
KeYmaera

Webstart KeYmaera

If you want to try a simple version of KeYmaera quickly without having to install it, use the KeYmaera Webstart. The webstart version provides most but not all features of KeYmaera. If you want the full verification power, we recommend that you download and install KeYmaera on your computer. The KeYmaera Webstart is simpler to set up.

Requirements and Add-ons:

Java 1.5+
Mathematica (optional, recommended)
Reduce/Redlog (optional)
QEPCAD B or QEPCAD B for Mac (optional)
HOL Light (optional)
Cohen-Hörmander Quantifier Elimination (optional)
CSDP (optional)

Download KeYmaera & Documentation

The simplemost way to run KeYmaera, generally is to use the KeYmaera Webstart. If you experience problems with the webstart or want to use some of the features that are only available in the download version, read on. KeYmaera is distributed under the GNU General Public License.

The full version of KeYmaera with all features and full verification support can be installed on your computer as follows:

Download KeYmaera Installer and run by double clicking, or webstart KeYmaera Installer to install KeYmaera on your computer.
Download KeYmaera Examples.
See user guide for more information and documentation on how to use KeYmaera.
Please direct questions to the KeYmaera mailing list.
Obtain KeYmaera Sources.

Requirements and Add-ons:

Java 1.5+
Mathematica (optional, recommended)
Reduce/Redlog (optional)
QEPCAD B or QEPCAD B for Mac (optional)
HOL Light (optional)
Cohen-Hörmander Quantifier Elimination (optional)
CSDP (optional)

KeYmaera Setup and Configuration

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.

Mathematica (optional, recommended) When KeYmaera starts, it asks for the path to the J/Link native library directory where the file JLink.jar can be found. For instance, for Mac OS X you would enter one of the following (depending on whether you are using a 32bit or 64bit Java Virtual Machine):
```
  /Applications/Mathematica.app/SystemFiles/Links/JLink/SystemFiles/Libraries/MacOSX-x86
```
```
  /Applications/Mathematica.app/SystemFiles/Links/JLink/SystemFiles/Libraries/MacOSX-x86-64
```
Next, it asks for the path to the MathKernel executable of Mathematica. For instance, for Mac you would enter:
```
  /Applications/Mathematica.app/Contents/MacOS/MathKernel
```
Reduce/Redlog (optional) When KeYmaera starts it asks for the path to the Reduce/Redlog executable reduce.
QEPCAD B or QEPCAD B for Mac (optional) When KeYmaera starts it asks for the path to the QEPCAD directory qesource and the saclib library that comes with QEPCAD.

You can configure any number of these tools. Later on, you can change the configuration in the "Hybrid Strategy" tab. You choose which solvers to use and change path settings later on at the bottom in "Mathematica Options", "Qepcad Options", "Reduce Options" tabs. Note that you may have to restart KeYmaera if you change the JLink library path.

Support

Send an email to KeYmaera mailing list
KeYmaera feature request & bug tracker

Developers

KeYmaera has been developed in the group of Prof. Ernst-Rüdiger Olderog at the University of Oldenburg and of André Platzer at Carnegie Mellon University. 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, and Prof. Bernhard Beckert at the University of Koblenz. The main KeYmaera developers are:

André Platzer, Carnegie Mellon University
Jan-David Quesel, University of Oldenburg
Philipp Rümmer, Oxford University Computing Laboratory