loading...
Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes
Koblenz, Germany September 07-September 09
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.51Third IEEE International Conference o ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Dirk Leinenbach, Wolfgang Paul, Elena Petrova, "Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes," Software Engineering and Formal Methods, International Conference on, pp. 2-12, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005.
 
 
BibTex
x
 
@article{ 10.1109/SEFM.2005.51,
author = {Dirk Leinenbach and Wolfgang Paul and Elena Petrova},
title = {Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes},
journal ={Software Engineering and Formal Methods, International Conference on},
volume = {0},
year = {2005},
isbn = {0-7695-2435-4},
pages = {2-12},
doi = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.51},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Software Engineering and Formal Methods, International Conference on
TI - Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes
SN - 0-7695-2435-4
SP2
EP12
A1 - Dirk Leinenbach,
A1 - Wolfgang Paul,
A1 - Elena Petrova,
PY - 2005
KW - null
VL - 0
JA - Software Engineering and Formal Methods, International Conference on
ER -
 
Dirk Leinenbach, Saarland University, Germany
Wolfgang Paul, Saarland University, Germany
Elena Petrova, Saarland University, Germany
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.
Citation:
Dirk Leinenbach, Wolfgang Paul, Elena Petrova, "Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes," sefm, pp.2-12, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.