Download 3rd Party Software
Libraries (required)
In order to run KeY the following 3rd-party libraries are required: Recoder*) (LGPL), TU Dresden OCL Parser*) (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 for download in this single package.
*) These libraries have been modified by the KeY team. The sources of our modifications are available upon request.
Add-Ons
- Grammatical Framework introduces natural language support for creating formal specifications. GF has been developed by Aarne Ranta's group at Chalmers University. More information about the translation tool here. Download GF-based binaries or sources here.
- 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 since version 1.0.0 KeY supports several SMT-LIB capable provers like
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.