Semesterarbeit

Proof-transforming compilers (PTC) are similar to certifying compilers in proof-carrying code, but take a source proof as input and produce the bytecode proof. An important property of proof-transforming compilers is that they do not have to be trusted. If the compiler produces a wrong specification or a wrong proof for a component, the proof checker of the component platform will reject the component.

Goal of the semester project is to implement a proof-transforming compiler from Eiffel to .Net CIL. The source languge is a subset of Eiffel, the logic for the subset of Eiffel is a Hoare style logic. The bytecode language is .Net CIL.

projectplan
report