[an error occurred while processing this directive]


Type of project:
Master Thesis February - August 2008

Manuel Hess

Integrating Proof-Transforming Compilation into EiffelStudio

Supervising Assistant:
Martin Nordio


Proof-Carrying Code is a technique that allows one to execute mobile code in a safe way. To produce the proof automatically, Certifying Compilers can be used. However, proof can only be generated automatically for a restricted set of properties (e.g type safe properties).

A proof-transforming compiler (PTC) is a compiler that takes a source proof as input and produces a bytecode proof. Using this approach, we can generate a proof in the source language (which is simpler than generating the proof in the bytecode level) and translate it to bytecode.

This project consists of the integration of a proof-transforming compiler for Eiffel into Eiffel Studio. The compiler takes a source proof in XML format and produces the bytecode proof. The source proofs are generated automatically using Ballet. The project will investigate the integration of the proof-transforming compiler with Ballet.