Title: Towards the formal verification of a C0 compiler: code generation and implementation correctness
Abstract: 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 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.
Publication Year: 2005
Publication Date: 2005-01-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 94
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot