Masterarbeit

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.

projectplan
report