The Community for Technology Leaders
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2005)
Koblenz, Germany
Sept. 7, 2005 to Sept. 9, 2005
ISBN: 0-7695-2435-4
pp: 2-12
Elena Petrova , Saarland University, Germany
Wolfgang Paul , Saarland University, Germany
Dirk Leinenbach , Saarland University, Germany
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.
INDEX TERMS
null
CITATION
Elena Petrova, Wolfgang Paul, Dirk 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'05), vol. 00, no. , pp. 2-12, 2005, doi:10.1109/SEFM.2005.51
93 ms
(Ver 3.3 (11022016))