KeY - VSTTE 12

On 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 Casts

They show how the automatic proof strategy finds the proofs and how long it takes.


The 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
    into your console and press enter.
After its first download, you can run KeY without any internet connection (see section "Frequently Asked Questions")

Binary and Source Code Distribution

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:

Frequently Asked Questions

  1. 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.
  2. 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 -version
    produces an output close to
    Java(TM) SE Runtime Environment (build 1.6.0_xyz)
    Java HotSpot(TM) Client/Server VM
    Please ensure also that javac refers to the Sun Java compiler and not to ejc or 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