Krakatoa
Krakatoa is a verification tool for Java programs. It is a tool from the Why platform for deductive program verification.
The current version 2.18 is a major reimplementation of the older 0.67 which is still available here
Documentation
Documentation is available in PDF format or in online HTML
Here are a few closely related academic papers:
- Lecture notes, slides, and exercises of the Winter School on Verification
of Object-Oriented Programs are available on this page
- The foundations of Krakatoa are described in ``The Krakatoa
tool for certification of Java/JavaCard programs annotated in
JML''. Journal of Logic and Algebraic Programming, 58(1-2):89-106,
2004
- More technical details on the memory modeling is given in
``Reasoning about Java programs with aliasing and frame conditions''. In
J. Hurd and T. Melham, editors, 18th International Conference on
Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes
in Computer Science. Springer, August 2005.
- A specific paper about handling JavaCard transaction mechanism is
``Verification of Java Card applets behavior with respect to
transactions and card tears''. In Dang Van Hung and Paritosh Pandya,
editors, 4th IEEE International Conference on Software Engineering and
Formal Methods (SEFM'06), Pune, India, September 2006. IEEE
Comp. Soc. Press.
- See also the tool presentation at
CAV 2007:
The
Why/Krakatoa/Caduceus platform for deductive program verification
Download
Krakatoa is freely available under the terms of the GNU GENERAL PUBLIC LICENSE.
Current version is 2.18 and is released together with Why
version 2.18. You can download from
here.
Contact
There is a
mailing
list for the Why plaform (to ask questions about Krakatoa, to get
announces of new releases, etc.).
There is also a bug tracking system. For
security reasons, you need to register before submitting a new
bug. Please create an account there, where you can put "ProVal" for
the required field "INRIA Research Project you work with or work in".
Related tools
30/1/2009