SCT Student Projects - Ghislain Fourny

Abstract: The new version of Jive takes JML-annotated Java programs as input. After an introduction to Jive and details about the JML specification and implementation, this paper describes the internal implementation of the Proof Obligation Generator in Jive's front-end, as well as its external (input and output) interfaces. We then give some examples of code we performed tests against.