|
KeYmaera
or Source |
||
|
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]
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.
- Download KeYmaera Installer and click on the downloaded JAR file to run it.
- To start KeYmaera Installer, you may have to right-click the jar file and choose Open.
You can also run it from command-line via:
java -jar keymaera-installer.jar
- Running the KeYmaera Installer again is also the best way of starting KeYmaera on your computer every time you want to use it. The KeYmaera Installer will run your local copy of KeYmaera and, if you wish, will also check whether updates are available.
- If you are behind a company firewall that is limiting your access to the web, follow these directions to configure a proxy for your firewall.
Requirements and Add-ons:
- Java 1.6+, 64bit (required)
- Mathematica (optional, recommended)
- Z3 SMT Solver by Microsoft Research (auto-install, optional)
-
Reduce/Redlog (auto-install, optional)
Be sure to install an X11 server to be able to use redlog - MetiTarski solver (optional but recommended for transcendental functions)
- QEPCAD B or QEPCAD B for Mac (optional)
- HOL Light (optional)
- Cohen-Hörmander Quantifier Elimination (optional)
- CSDP (auto-install, optional)
Once KeYmaera is up and running you can look at examples to get started, for instance:
- File->Load Project
- Choose Simple Acceleration example
- Click Proof->Start to start the automatic prover
- File->Load Project
- File->Start Tutorial
KeYmaera Extras
KeYmaera is distributed under the GNU General Public License.
- Download Sphinx: Verification-Driven Engineering Toolkit for KeYmaera
- Download KeYmaera vi mode
- Examples are available in KeYmaera in the project manager menu item File->Load Project
- See user guide for more information and documentation on how to use KeYmaera.
- In KeYmaera, menu item File->Start Tutorial shows the tutorial that will take you through a number of steps for learning KeYmaera.
- Please direct questions to the KeYmaera mailing list.
- Obtain KeYmaera Source Code.
-
We would appreciate if you could introduce yourself and tell us about how your are using KeYmaera.
Send email to the KeYmaera mailing list.
- Java 1.5+
- Mathematica (optional, recommended)
- Z3 SMT Solver by Microsoft Research (auto-install, optional)
-
Reduce/Redlog (auto-install, optional)
Be sure to install an X11 server to be able to use redlog - MetiTarski solver for transcendental functions (optional but recommended for transcendental functions)
- QEPCAD B or QEPCAD B for Mac (optional)
- HOL Light (optional)
- Cohen-Hörmander Quantifier Elimination (optional)
- CSDP (auto-install, optional)
Support
- Send an email to KeYmaera mailing list
- KeYmaera feature request & bug tracker
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:- Stefan Mitsch, Carnegie Mellon University
- André Platzer, Carnegie Mellon University
- Jan-David Quesel, Carnegie Mellon University (previously University of Oldenburg, Germany)
- Khalil Ghorbal, Carnegie Mellon University (differential radical invariants and advanced equational differential invariants)
- Andrew Sogokon, University of Edinburgh, UK (MetiTarski integration and transcendental functions, non-smooth barrier certificates and advanced equational differential invariants)
- Stefan Mitsch and Il Suk Lyu, Carnegie Mellon University (simulation engine for hybrid programs)
- Philipp Rümmer, Uppsala University, Sweden (built-in Gröbner basis and Fourier-Motzkin arithmetic)
- David Renshaw, Carnegie Mellon University (Cohen-Hörmander arithmetic)
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.- 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.