KeY 1.6.5
For getting KeY 1.6.5, choose one of the following options:
- Start it directly via Web Start[?] using the "Run KeY 1.6.5" link on the right
- Download the pre-compiled bytecode version: KeY-1.6.5.tgz or KeY-1.6.5.zip, README-1.6.5.txt, required libraries
- Compile it from source: KeY-1.6.5-src.tgz, README-1.6.5-src.txt, required libraries
New Features in 1.6.5
- Support for Strings
- Enhanced JML support
- Improved integration of external SMT solvers
- Improved "verification-based testing" mechanism
- Real Time Java (RTSJ) calculus
- GUI improvements
- Various bugfixes
Addons
KeY can optionally use SMT solvers to improve automation: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.
Examples and Documentation
- A collection of examples (already included in bytecode and sourcecode distribution): examples-1.6.zip
- The best source for information on KeY is the KeY Book. In particular, chapter 10 provides a thorough introduction to the system. We provide also updated examples of the KeY Book for KeY-1.6.0 (BookExamples-1.6.zip)
- There are several case studies and tutorials that introduce to the main functions of KeY and show how KeY handles more extensive contexts. In particular, we recommend the KeY Quicktour as an introduction. The examples for the Quicktour can be found here.
- A cheat sheet for the KeY-Syntax (draft).