Winter School: instruction for lab session/Krakatoa tool

There is a lecture about Krakatoa in the Winter School on Verification of Object-Oriented Programs.
This web page is dedicated to instructions for running the Krakatoa tool and doing exercises for the lab session. Krakatoa is one particular tool available inside the Why platform, so installing Krakatoa amounts to install Why. Moreover, the platform is able to call a family of external provers, which must be installed independently.
  1. Lectures
  2. Exercices
  3. Installing Provers
  4. Installing Krakatoa
  5. Eclipse Plugin
Please report installation problems but also successful installation to Claude Marché

Lectures

Exercices

Installing Provers

Please install as many provers as possible from the following list, and at least Simplify and Alt-ergo. Note: for use of proof assistant such as Coq or PVS, see why web page. Only automatic provers will be used during the school.

Installing Krakatoa

Krakatoa is primarily developed for running under Unix platforms. Some partial support is also provided for Microsoft Windows. It is recommended to install the new version 2.18 of Why and Krakatoa

Precompiled binaries

Installing a precompiled binary is of course much easier, but may fail if your architecture is not well supported.

Compilation from sources

Compilation from sources amount to uncompress the sources and do
./configure
make
sudo make install
See remarks above for changing the default destination directory.

This will work only if proper development tools are installed first:

Here are some hints to setup a proper environment:

Testing installed Krakatoa

To test your installation, you should run
gwhy Isqrt.java
on that Isqrt.java file and in the GUI, click on buttons "Simplify" and "Alt-Ergo" at top of columns of the table on the left. You should obtain the following:

Eclipse plugin

For Eclipse fans, there is an Eclipse Plugin for the Why platform. Note that a few minor features are missing w.r.t to the dedicated GWhy interface.
30/1/2009