Paper Info
Title
Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes
Abstract
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 C0 (a subset of C which is similar to MISRA C [20]). This paper reports on (i) an operational small steps semantics for C0 which is formalized in Isabelle/HOL [25], (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.
Year
DOI
Venue
2005
10.1109/SEFM.2005.51
SEFM
Keywords
Field
DocType
formal verification effort,verisoft project,formal proof,code generation,pencil correctness proof,formal specification,c0 compiler,pervasive verification,misra c,dlx machine language,paper report,main programming language,implementation correctnes,formal verification
Functional compiler,Programming language,Computer science,Correctness,Compiler correctness,Formal specification,Theoretical computer science,Compiler,Compiler construction,Formal methods,Formal verification
Conference
ISBN
Citations 
PageRank 
0-7695-2435-4
39
3.52
References 
Authors
18
3
Name
Order
Citations
PageRank
Dirk Leinenbach153427.36
Wolfgang Paul2454.39
Elena Petrova31447.65