This paper presents the formal Isabelle/HOL framework we use to prove refinement between an executable, monadic specification and the C implementation of the seL4 microkernel. We describe the refinement framework itself, the automated tactics it supports, and the connection to our previous C verification framework. We also report on our experience in applying the framework to seL4. The characteristics of this microkernel verification are the size of the target (8,700 lines of C code), the treatment of low-level programming constructs, the focus on high performance, and the large subset of the C programming language addressed, which includes pointer arithmetic and type-unsafe code.

@InProceedings{Winwood_KSACN_09,
    author =    {Simon Winwood and Gerwin Klein and Thomas Sewell and 
                 June Andronick and David Cock and Michael Norrish},
    title =     {Mind the Gap: A Verification Framework for Low-Level {C}},
    booktitle = {Proc.\ 22nd TPHOLs},
    editor =    {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
    year =         {2009},
    address =      {Munich, Germany},
    pages =        {500-515},
    month =        Aug,
    series =       {Lecture Notes in Computer Science},
    volume =       {5674},
    publisher =    {Springer},
}