Jahob Verification System
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
- Information below may be outdated
- Java may be outdated. Consider Scala, http://www.scala-lang.org/
- To verify Scala, consider tools such as http://leon.epfl.ch and its successors
Some of the data structures verified in 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.
Architecture of a Part of Jahob
A Few Simple Jahob examples
Here are some small examples that illustrate Jahob's specification constructs.
Many more verified examples are available in Jahob distribution.
Current Snapshot of the System
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.
- External tools:
To get started with proving formulas:
- download and make formDecider
- download or make the cvc3 executable
- add the binaries from Jahob and CVC3 to your path
- to prove a formula using formDecider from Jahob using the CVC3 prover, invoke
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:
- Modular Data Structure Verification (PhD dissertation, MIT 2007)
A link to internal discussion page
Jahob project is supported by the funding from the US and Swiss National Science Foundations.