SCT Student Projects - Yoshimi Takano

The goal of this master’s project is the implementation of uniqueness and ownership transfer in the JML Compiler as extension to the Universe Type System. Since destructive reads change the semantics of the programming language and are unintuitive for programmers, it is desirable to replace them by developing a modular, static data flow analysis ensuring that no destructive reads are needed.

The Java Interactive Verification Environment, Jive, is a verification system for objectoriented programs on the basis of a partial-correctness Hoare-style programming logic. The verification of general lemmas that arise during a program proof is delegated and performed by an associated general theorem prover. Currently, the interactive theorem prover Isabelle is supported for this purpose. This report describes the integration of the fully automatic theorem prover Simplify as an additional associated theorem prover.