Download 3rd Party Software
Libraries (required)
In order to run KeY the following 3rd-party libraries are required: Recoder* (LGPL), Xerces (Apache License), ANTLR (Public Domain), JavaCC (BSD License), JUnit (IBM Common Public License), JArgs (BSD License), Log4J (Apache License).
We are providing these libraries as a single package: KeYExtLib-1.4.tgz or KeYExtLib-1.4.zip
These libraries and an additional library for Verification-based Testing is provided in the "Nightly Builds" package: KeYExtLib-1.5NB.tgz or KeYExtLib-1.5NB.zip
*) These libraries have been modified by the KeY team. The sources of our modifications are available upon request.
Add-Ons (optional)
- Simplify is a decision procedure used to solve (many) arithmetical sub-problems automatically. Simplify has been developed at Compaq by Dave Detlefs, Greg Nelson, and Jim Saxe. It is currently maintained by KindSoftware. Download Simplify binaries (version 1.5.4) for Linux, MacOS X (PPC), Windows.
- SMT-LIB provers supported
by KeY:
In addition, KeY provides an export into the SMT-LIB input file format, which can be used by any decision procedure supporting this format. Bindings for new decision procedures can be added easily, in case of interest please ask the KeY group for assistance.