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:
  1. 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.
  2. 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
M. Sc. Abdul Qadar Kara
Dr. Dirk Leinenbach
Dr. Hristo Pentchev
Dr. Elena Petrova
Verena Kremer