|
Launch KeYmaera |
||
Webstart KeYmaeraWe 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:
As a simple example, you can look at the following:
Download KeYmaera & DocumentationThe 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:
|
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
- 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.
- 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.
