Download KeYmaera Verification Tool for Hybrid Systems

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

Webstart KeYmaera

We recommend to start KeYmaera just by running the KeYmaera Webstart, version 3.5. The webstart version provides all features of the installed KeYmaera version and is easier to set up.

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

Download KeYmaera

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 contributions from:

Older Versions: KeYmaera 1.5-3.4

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.