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.

• Screencast for Problem 1
• Screencast for Problem 3

Solutions

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 javaws https://www.key-project.org/vstte12/webstart/KeY.jnlp 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

• 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

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