Download KeYmaera Verification Tool for Hybrid Systems

  1. Home
  2. >>
  3. Tools
  4. >>
  5. KeYmaera
  6. >>
  7. Download
Table of Contents
  1. Outdated
  2. Download KeYmaera Installer
  3. KeYmaera Extras
  4. Support
  5. Developers
  6. Older Versions: KeYmaera 1.5-3.2
KeYmaera or
Source
Book: Logical Analysis of Hybrid Systems

Outdated

The successor, KeYmaera X, is an entirely new and overall better theorem prover for hybrid systems building on the experience with the successes of KeYmaera. The older KeYmaera prover is, of course, also still available, but we generally recommend KeYmaera X for most purposes. [comparison]

 

See Successor: KeYmaera X

 

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

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 Chalmers University of Technology in Gothenburg (now TU Darmstadt), and Prof. Bernhard Beckert at the University of Koblenz (now KIT). 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.