SCT Student Projects - Erich Laube

Abstract: At the ETH in Zurich, research is being done on semi-automatic verification of Java code. Part of this research is a tool called Jive (Java Interactive Verification Environment). Jive only handles a subset of the Java language, called Diet Java Card (DJC). This work describes the transformations I implemented to translate normal Java code into this subset.