The Jive Tool

This page contains information about the Java Interactive Verification Environment, Jive for short.

Members

  • Prof. Dr. Arnd Poetzsch-Heffter, TU Kaiserslautern, AG Softwaretechnik
  • Ass. Prof. Dr. Peter Müller, ETH Zürich

Abstract

Jive is a verification system that is being developed at the University of Kaiserslautern and at the ETH Zürich. It is an interactive special-purpose theorem prover for the verification of object-oriented programs on the basis of a partial- correctness Hoare-style programming logic. Jive operates on Java-KEx, a desugared subset of sequential Java which contains all important features of object-oriented languages (subtyping, exceptions, static and dynamic method invocation, etc.). Jive is written in Java and currently has a size of about 40,000 lines of code.

Jive is able to operate on completely unannotated programs, allowing the user to dynamically add specifications. It is also possible to preliminarily annotate programs with invariants, pre- and postconditions using the specification language JML. In practice, a mixture of both techniques is employed, in which the user extends and refines the pre-annotated specifications during the verification process. The program to be verified, together with the specifications, is translated to Hoare sequents. Program and pre-annotated specifications are translated during startup, while the dynamically added specifications are translated whenever they are entered by the user. Hoare sequents have the shape A |> { P } pp { Q } and express that for all states S that fulfill P, if the execution of the program part pp terminates, the state that is reached when pp has been evaluated in S must fulfill Q. The so-called assumptions A are used to prove recursive methods.

Jive’s logic contains so-called Hoare rules and axioms. The rules consist of one or more Hoare sequents that represent the assumptions of the rule, and a Hoare sequent which is the conclusion of the rule. Axioms consist of only one Hoare sequent; they do not have assumptions. Therefore, axioms represent the known facts of the Hoare logic.

To prove a program specification, the user directly works on the program source code. Proofs can be performed in backward direction and in forward direction. In backward direction, an initial open proof goal is reduced to new, smaller open subgoals by applying a rule. This process is repeated for the smaller subgoals until eventually each open subgoal can be closed by the application of an axiom. If all open subgoals are proven by axioms, the initial goal is proven as well.

In forward direction, the axioms can be used to establish known facts about the statements of a given program. The rules are then used to produce new facts from these already known facts. This way, facts can be constructed for parts of the program.

Researchers in AG Softech

  • Prof. Dr. Arnd Poetzsch-Heffter
  • Dipl.-Inform. Nicole Rauch
  • Dipl.-Inf. Jean-Marie Gaillourdet
  • Jan Schäfer

Funding

Completion Status