Download 3rd Party Software
Libraries (required)
In order to run KeY, the following 3rd-party libraries are required: Recoder (LGPL; modified by KeY team, sources of our changes available upon request), ANTLR (Public Domain). For compiling the source code distribution, and for using KeY's verification based testing facilities, additional libraries are needed.
We are providing all of these libraries as a single package: KeYExtLib-1.6.tgz or KeYExtLib-1.6.zip
Older library package for KeY 1.5 nightly build versions: KeYExtLib-1.5NB.tgz or KeYExtLib-1.5NB.zip
Add-Ons (optional)
Optionally, KeY can make use of a number of external SMT solvers, namely
In addition to directly supporting these solvers, KeY provides an export into the SMT-LIB file format. Bindings for new SMT solvers supporting this format can be added easily, in case of interest please ask the KeY group for assistance.