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

• 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

• ArrayList class JavaDoc to
• a verified ArrayList interface from an earlier version of the verified data structures above

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.

• Bank account example in Jahob
• Simple linked list operation in Jahob

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.

• Jahob sources, examples, some bytecode and binaries
• Jahob windows binaries and sources
• External tools:
  • Some of the external binaries
  • CVC3
  • Z3 linux version, or Z3 official distribution
  • Isabelle interactive theorem prover
  • Decision procedure for weak monadic second-order logic over trees
  • E prover

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.

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:

• Andreas Podelski, Thomas Wies: Counterexample-Guided Focus (POPL), 2010.
• Karen Zee, Viktor Kuncak, and Martin Rinard. An integrated proof language for imperative programs. In ACM Conf. Programming Language Design and Implementation (PLDI), 2009.
• Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In ACM Conf. Programming Language Design and Implementation (PLDI), 2008.
• Charles Bouillaguet, Viktor Kuncak, Thomas Wies, Karen Zee, and Martin Rinard. Using first-order theorem provers in the Jahob data structure verification system. In Verification, Model Checking and Abstract Interpretation, volume 4349 of LNCS, November 2007.
• Modular Data Structure Verification (PhD dissertation, MIT 2007)
• Thomas Wies, Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard. Field constraint analysis. In Proc. Int. Conf. Verification, Model Checking, and Abstract Interpratation, volume 3855 of LNCS, 2006.
• Thomas Wies, Viktor Kuncak, Karen Zee, Andreas Podelski, and Martin Rinard. Verifying complex properties using symbolic shape analysis. In Workshop on Heap Abstraction and Verification (collocated with ETAPS), 2007.
• Viktor Kuncak, Huu Hai Nguyen, and Martin Rinard. An algorithm for deciding BAPA: Boolean Algebra with Presburger Arithmetic. In 20th International Conference on Automated Deduction, CADE-20, volume 3632 of LNCS, Tallinn, Estonia, July 2005.

A link to internal discussion page

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