Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2005)
Sept. 7, 2005 to Sept. 9, 2005
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.51
Dirk Leinenbach , Saarland University, Germany
Wolfgang Paul , Saarland University, Germany
Elena Petrova , Saarland University, Germany
In the spirit of the famous CLI stack project  the Verisoft project  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 C0 (a subset of C which is similar to MISRA C ). This paper reports on (i) an operational small steps semantics for C0 which is formalized in Isabelle/HOL , (ii) the formal specification of a compiler from C0 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 C0 and a formal proof in Isabelle/HOL that the implementation produces the same code as the specification.
E. Petrova, W. Paul and D. Leinenbach, "Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes," Third IEEE International Conference on Software Engineering and Formal Methods(SEFM), Koblenz, 2005, pp. 2-12.