LARA

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

Note


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.

Click for Jahob Screenshot

Architecture of a Part of Jahob

Jahob Architecture

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.

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
    bin/decide example.form

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.

LICENCE

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.

Selected Publications

Jahob discussion

A link to internal discussion page

Acknowledgements

Jahob project is supported by the funding from the US and Swiss National Science Foundations.