Proof Generating Compiler

This page contains information about Proof Generating Compiler, ProGenCo for short.

Members

• Prof. Dr. Arnd Poetzsch-Heffter, TU Kaiserslautern, AG Softwaretechnik

Abstract

The goal of the project is the development of a formal method for the translation verification. The method builds on a translation validation technique in which the checking of the translation of the translation is realized as proof checking within an external specification and verification framework, SVF for short. Based on formal specifications of source and target language and a translation predicate in the SVF, the compilers produce, in addition to the target program T, a proof that T is correct w.r.t. its source program.

We use ML as an implementation language and the theorem prover Isabelle/HOL as SVF.

Researchers in AG Softech

• Prof. Dr. Arnd Poetzsch-Heffter
• Dipl.-Inform. Marek Jerzy Gawkowski
• Dipl.-Inform. Jan Olaf Blech

Funding

The described project is funded by the state of Rhineland-Palatinate.

Completion Status

Started January 2004