Towards the formal verification of a C0 compiler: Code generation and implementation correctness

In the spirit of the famous CLI stack project [2] the Verisoft project [31] aims at the pervasive verification of entire computer systems including hardware, system software, compiler, and communicating applications, with a special focus on industrial applications. The main programming language used in the Verisoft project is CO (a subset of C which is similar to MISRA C [20]). This paper reports on (i) an operational small steps semantics for CO which is formalized in Isabelle/HOL [25], (ii) the formal specification of a compiler from CO to the DLX machine language [14,23] in Isabelle/HOL, (iii) a paper and pencil correctness proof for this compiler and the status of the formal verification effort for this proof and (iv) the implementation of the compiler in CO and a formal proof in Isabelle/HOL that the implementation produces the same code as the specification.