
Masterarbeit

ProofCarrying 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 prooftransforming 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 prooftransforming 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 prooftransforming compiler with Ballet. 