KeY - VSTTE 12On this website you find the problem solutions submitted to the VSTTE 12 competition as well as the used KeY version. For the competition, we used a special patched development version of KeY.
Screen CastsThey show how the automatic proof strategy finds the proofs and how long it takes.
SolutionsThe solutions for problems 1, 3, and 4 have been written in Java + JML and verified using KeY. Here you can download all solutions along with KeY proof files. (You may need a special version of KeY, see below). The package also contains a README file with hints on how to read the specs and how to replay the proofs.
Web Start (recommended)We recommend to install and run KeY via Java Web Start. On most systems, Java Web Start should already be installed together with the Java SDK.
- Click Start KeY to run the KeY Tool.
- Alternatively, you can enter the following line
javaws http://www.key-project.org/vstte12/webstart/KeY.jnlpinto your console and press enter.
Binary and Source Code Distribution
- Download the pre-compiled bytecode version and proceed as described in the readme file: KeY-vstte.tgz README.txt, external libraries (choose nightly builds libraries (KeYExtLib-1.5NB)
- Compile KeY from source and proceed as described in the readme file: KeY-SEFM2010-src.tgz, README-src.txt, external libraries (choose nightly-build libraries (KeYExtLib-1.5NB)
Alternatively, you can compile the current stable version 2.2 after applying this patch, which introduces additional rules.
Additional 3rd Party Tools
Optionally, you can choose amongst several supported SMT provers:
- External add-ons (Simplify, SMT-LIB provers)
Frequently Asked Questions
- Do I need online access for Java Web Start? Only the first time, afterwards you can run Java Web Start javaws -viewer (Java 6) resp. javaws (Java 5). Select then KeY from the upcoming list of applications and Run Offline.
- I get some strange error message with gij
mentioned. Please check that you have installed the
SunJDK 6 (or 5) and that you selected them as your main
Java environment. Executing the command
Java(TM) SE Runtime Environment (build 1.6.0_xyz)Please ensure also that
Java HotSpot(TM) Client/Server VM
javacrefers to the Sun Java compiler and not to
gij. On Ubuntu you can change the default Java SDK via sudo update-alternatives --config java and sudo update-alternatives --config javac
Similarly, make sure that you run the Sun version of javaws, via: sudo update-alternatives --config javaws