Paper Info
Title
Pervasive Compiler Verification -- From Verified Programs to Verified Systems
Abstract
We report in this paper on the formal verification of a simple compiler for the C-like programming language C0. The compiler correctness proof meets the special requirements of pervasive system verification and allows to transfer correctness properties from the C0 layer to the assembler and hardware layers. The compiler verification is split into two parts: the correctness of the compiling specification (which can be translated to executable ML code via Isabelle's code generator) and the correctness of a C0 implementation of this specification. We also sketch a method to solve the boot strap problem, i.e., how to obtain a trustworthy binary of the C0 compiler from its C0 implementation. Ultimately, this allows to prove pervasively the correctness of compiled C0 programs in the real system.
Year
DOI
Venue
2008
10.1016/j.entcs.2008.06.040
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
compiler verification,c0 layer,pervasive compiler verification,system verification,verified systems,hoare logic,hol,correctness property,formal verification,theorem proving,compiler correctness proof,c0 implementation,simple compiler,c0 program,c-like programming language c0,verified programs,c0 compiler,code generation,programming language
Functional compiler,Programming language,Computer science,Compiler correctness,Correctness,Theoretical computer science,Code generation,Compiler,Compiler construction,High-level verification,Formal verification
Journal
Volume
ISSN
Citations 
217,
Electronic Notes in Theoretical Computer Science
18
PageRank 
References 
Authors
1.05
25
2
Name
Order
Citations
PageRank
Dirk Leinenbach153427.36
Elena Petrova21447.65