Download KeYmaera Verification Tool for Hybrid Systems

Table of Contents Webstart KeYmaera Download KeYmaera & Documentation Support Developers Older Versions: KeYmaera 1.5

Launch KeYmaera

Webstart KeYmaera We recommend to start KeYmaera just by running the KeYmaera Webstart. The webstart version provides all features of the installed KeYmaera version and is easier 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) As a simple example, you can look at the following: File->Load Project Choose Simple Acceleration example --> Click Proof->Start to start the automatic prover Download KeYmaera & Documentation The simple most way to run KeYmaera is to use the KeYmaera Webstart. If you experience problems with the webstart, read on. KeYmaera is distributed under the GNU General Public License. It can be installed 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)

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 Prof. 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

With contributions from:

• David Renshaw, Carnegie Mellon University

Older Versions: KeYmaera 1.5

In order to run the older release KeYmaera 1.5 use the KeYmaera 1.5 Webstart. If you experience problems with the webstart, you can also install the older release KeYmaera 1.5:

• Download KeYmaera 1.5 Installer and run by double clicking, or webstart KeYmaera 1.5 Installer to install KeYmaera 1.5 on your computer.
• Download KeYmaera Examples.

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, KeYmaera 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.