====== 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 * 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 ---- [[data_structure_examples.html|Some of the data structures verified in Jahob]] You may wish to compare * [[http://java.sun.com/j2se/1.4.2/docs/api/java/util/ArrayList.html#method_summary|ArrayList class JavaDoc]] to * [[http://lara.epfl.ch/~kuncak/jahob/ds/ArrayList/Spec-ArrayList.java|a verified ArrayList interface]] from [[http://lara.epfl.ch/~kuncak/jahob/ds/index.html|an earlier version]] of [[data_structure_examples.html|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. {{jahob-xsymbol-screenshot.png?400|Click for Jahob Screenshot}} ==== Architecture of a Part of Jahob ===== {{jahob-architecture.png?800|Jahob Architecture}} ==== A Few Simple Jahob examples ==== 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. ==== 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. * [[http://lara.epfl.ch/~kuncak/jahob/jahob.tar.gz|Jahob sources, examples, some bytecode and binaries]] * [[http://lara.epfl.ch/~kuncak/jahob/jahob-win-binaries.zip|Jahob windows binaries and sources]] * External tools: * [[http://lara.epfl.ch/~kuncak/jahob/jahob-external-bins.tar.gz|Some of the external binaries]] * [[http://www.cs.nyu.edu/acsys/cvc3/|CVC3]] * [[http://smtcomp.org/solvers/z3.tar.gz|Z3 linux version]], or [[http://research.microsoft.com/research/downloads/details/5fdacfa1-6c93-4a16-a2ac-6f4775e8ad1e/details.aspx|Z3 official distribution]] * [[http://www.cl.cam.ac.uk/research/hvg/Isabelle/|Isabelle interactive theorem prover]] * [[http://www.brics.dk/mona/|Decision procedure for weak monadic second-order logic over trees]] * [[http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html|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. ==== 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 ==== Some relevant publications: * [[http://pub.ist.ac.at/~wies/papers/CounterexampleGuidedFocus.pdf|Andreas Podelski, Thomas Wies: Counterexample-Guided Focus (POPL), 2010.]] * [[http://lara.epfl.ch/~kuncak/papers/ZeeETAL09IntegratedProofLanguageforImperativePrograms.html|Karen Zee, Viktor Kuncak, and Martin Rinard. An integrated proof language for imperative programs. In ACM Conf. Programming Language Design and Implementation (PLDI), 2009.]] * [[http://lara.epfl.ch/~kuncak/papers/ZeeETAL08FullFunctionalVerificationofLinkedDataStructures.html|Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In ACM Conf. Programming Language Design and Implementation (PLDI), 2008.]] * [[http://lara.epfl.ch/~kuncak/papers/BouillaguetETAL07UsingFirstOrderTheoremProvers.html|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.]] * [[http://lara.epfl.ch/~kuncak/papers/Kuncak07DecisionProceduresModularDataStructureVerification.html|Modular Data Structure Verification]] (PhD dissertation, MIT 2007) * [[http://lara.epfl.ch/~kuncak/papers/WiesETAL06FieldConstraintAnalysis.html|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.]] * [[http://lara.epfl.ch/~kuncak/papers/WiesETAL06VerifyingComplexPropertiesSymbolicShapeAnalysis.html|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.]] * [[http://lara.epfl.ch/~kuncak/papers/KuncakETAL05AlgorithmDecidingBAPA.html|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.]] === Jahob discussion === A link to internal [[Jahob::discussion]] page ==== Acknowledgements ==== Jahob project is supported by the funding from the US and Swiss National Science Foundations.