Mind the Gap: Verification Framework for Low-Level C
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...[Show more]
|Collections||ANU Research Publications|
|Source:||Proceedings of International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009)|
|01_Winwood_Mind_the_Gap:_Verification_2009.pdf||584.92 kB||Adobe PDF||Request a copy|
|02_Winwood_Mind_the_Gap:_Verification_2009.pdf||105.66 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.