Jahob is a verification system for programs written in a subset of Java. Using Jahob, developers can statically prove that methods satisfy their contracts in all possible executions, as well as that they preserve essential structural invariants and design constraints.
Jahob is now on github: https://github.com/epfl-lara/jahob
You may wish to compare
The Jahob prototype is written mostly in Objective Caml. It was tested mostly on Debian GNU Linux distributions on a PC, but is expected to run under Windows and Mac as well.
Here are some small examples that illustrate Jahob's specification constructs.
Many more verified examples are available in Jahob distribution.
Here is one snapshot of the system. To try it, download the sources and run 'make'. If you do not have ocaml installed, download Jahob binaries and put them in your path. In any case, to make the system work, you will need to obtain some additional external decision procedures and provers.
To get started with proving formulas:
The bin/decide script invokes bin/formDecider with cvcl as the prover, see the script for the invocation. You should can build the OCaml bytecode version of formDecider using
cd src make -f Makefile.formDecider
or build the native code version using
cd src make -f Makefile.formDecider.opt
Here example.form is the file containing the formula you wish to prove in Isabelle-like notation.
We are happy to release Jahob software (specifically, the parts that we developed) under a variety of licences that suite your needs. Please contact us for further information if the default licence in the distribution is not adequate for you.
Some relevant publications:
A link to internal discussion page
Jahob project is supported by the funding from the US and Swiss National Science Foundations.