Skip to main content Skip to main navigation


Pervasive Compiler Verification - From Verified Programs to Verified Systems

Dirk Leinenbach; Elena Petrova
In: Ralf Huuck; Gerwin Klein; Bastian Schlich (Hrsg.). Proceedings of the 3rd International Workshop on Systems Software Verification. International Workshop on Systems Software Verification (SSV-08), 3rd, February 25-27, Sydney, NSW, Australia, Pages 23-40, Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 217, Elsevier Science B. V. 2008.


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.