|Chair of Programming Methodology|
SCT Student Projects - Alex Suzuki
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.
|Project Timeframe:||Winter semester 2004/05|
|Project Description:||PDF (German)|
|Supervisor:||Werner M. Dietl|
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.
|Project Timeframe:||April 2006 - September 2006|
|Last update: 08.11.2006 by email@example.com|