Institute for computer architecture and parallel computing

Main page

Project overview

We have formally verified a compiler for a C-like language (called C0) at the source code level. The proof has been divided into two major parts:

Formal specification of the code generation in the theorem prover Isabelle/HOL.
For this functional code generator we have proven that the generated code executed on an abstract assembly machine for the VAMP processor is a simulation of the execution of the C0 source code with the C0 small step semantics.
In the second part we have implemented the compiler in C0 and have proven that, for a given input program, this implementation produces the same assembly code as the functional compiler specification in Isabelle/HOL.

Project status

The project has been successfully completed. Formal artefacts, implementations, and documentation are available via the Verisoft Repository.

Project members