SCT Student Projects - Alex Suzuki

In this semester project the implementation of the Universe type system in the MultiJava and JML tools was extended to also emit type information into the Java bytecode.

Abstract: The goal of this semester project is to extend the MultiJava compiler to emit extensions used in the Universe type system into the generated Java class file. This involves finding a suitable binary representation for the extensions, and a means of storage which does not conflict with the Java class file format. This document presents a binary encoding of the Universe modifiers, and two possible approaches to their storage in the class file. Chapter 1 serves as an introduction to the problem of aliasing in object-oriented programming and gives a short introduction to the Universe type system. Chapter 2 gives an overview of the Java class file format and a quick introduction to the new J2SE 5.0 annotation facility. Chapter 3 provides a detailed look at our two implementation approaches, while chapter 4 provides an example. Chapter 5 describes the changes and extensions made to the MultiJava compiler. Chapter 6 then presents conclusions and possibilities for future work.

Master Project - Translating Java Bytecode to BoogiePL

Abstract: Boogie is a modular program verifier for verifying Spec# programs in the Microsoft .NET framework. The Spec# compiler generates CIL (Common Intermediate Language) bytecode from Spec# source code, a superset of C#, and transforms the resulting CIL to a guarded command language called BoogiePL. Boogie creates verification conditions from BoogiePL, and passes them to an automatic theorem prover, currently Simplify. While Boogie is part of the Spec# Programming System, there is no reason why it should not be leveraged to verify programs written in other object-oriented languages, namely Java, as long as we supply an appropriate transformation to BoogiePL. Also Spec# currently does not generate BoogiePL code for exception handling, so errors in exception handlers are currently not detectable by Boogie. This thesis presents a formalization in Coq of the translation from Java bytecode to BoogiePL, a guarded command language, including support for exceptions.