News Download Examples Related publications Other links

The Krakatoa Tool for Java Program Verification

The Java Modeling Language, JML for short, has been designed to formally specify the behaviour of Java programs. The Krakatoa tool allows one to certify that a JML-annotated method of a Java program meets its specifications. More precisely, it focuses on verifying the soundness of implementations with reference to pre/post-conditions (given in the specification) and class invariants. This amounts to proving that class invariants, as well as post-conditions, hold at the end of a method execution, provided that invariants and pre-conditions were valid at the beginning. The Krakatoa approach involves three distinct components: the Why tool, which computes proof obligations for a core imperative language annotated with pre and post conditions, the Coq proof assistant for modelisation of specifications and development of proofs, and finally the Krakatoa tool, which reads the Java files and produces specifications for Coq and a representation of the semantics of the Java program into Why's input language.

News

Release 0.67 is available. See CHANGES file.

Download

A preliminary release is now available. You can download below:

The source code, that must be compiled by
```
 
  ./configure 
  make
```
and installed by
```
  make install
```
to test your installation, do
```
  make -C test
```
The Windows binary, that is ready to be uncompressed in C:. Then add C:\krakatoa\bin in your PATH. The make tool is also necessary to use Krakatoa.
The documentation in PS or PDF format.

Please check the requirements mentioned in the documentation. This documentation also includes a small tutorial and a reference manual.

Examples

The distribution includes a small test suite. Here are some other examples of Java programs proved by Krakatoa.

Dijkstra's Dutch national flag
Sets of integers implemented by ordered arrays, including a binary search method
Knuth's algorithm for prime number based on Bertrand's postulate: available soon
Selection sort: available soon

Related publications

Short paper presenting the Krakatoa tool (a final version will appear in Journal of Logic and Algebraic Programming).
Paper presenting the memory model of Krakatoa (draft).
verisafe meeting, nice, september 19-20, 2002
- Abstract in Postscript
- Slides in PDF
- Slides in Postscript
- Animated slides using Active-DVI

A bit less scientific links

What happened to the Krakatoa volcano?
How to pronounce Krakatoa?
What movies have been made about Krakatoa?
Other images of the Volcano.

Generated on 24/1/2007

Do you want to have fun ? Click below on the language of your choice