The Jack tool provides an environment for verification of Java and Java Card programs with JML annotations. It implements a fully automated weakest precondition calculus that generates proof obligations from annotated Java sources. Those proof obligations can be discharged using different theorem provers.

JML verification for Java developers

An important design goal of Jack is that it is easy to use for normal Java developers, who use it to validate their own code. To allow developers to work in a familiar environment, Jack is integrated as a plugin in the eclipse IDE. Care has been taken to hide the mathematical complexity of the underlying concepts. Therefore Jack provides a dedicated proof obligation viewer, that presents the proof obligations connected to execution paths within the program. For each proof obligation, the relevant source code is highlighted. Moreover goals and hypothesis are displayed in a Java/JML like notation.

Our goal is to allow formal method experts to prove the correctness of Java applets, and moreover, to allow Java programmers to obtain a high confidence in the correctness of their application.

Proving program correctness

Currently proof obligations can be generated for The Jack proof manager sends the proof obligations to the different provers, and keeps track of proven and unproven proof obligations.

More information

Jack has been initially developed by the Research Laboratory at Gemplus and is now being developed within the Everest team at INRIA Sophia Antipolis, with partial support from the IST project INSPIRED, and of the ACI Sécurité GECCOO.

Jack is publicly available under a Cecill C licence.

If you want to keep in touch with Jack developements you can subscribe to the jack-interest@lists-sop.inria.fr mailing list.
To do so, simply send an email to sympa@lists-sop.inria.fr with the subject line 'subscribe jack-interest' (without the ').