Skip navigation
Skip navigation

Mind the Gap: Verification Framework for Low-Level C

Winwood, Simon; Klein, Gerwin; Sewell, Thomas; Andronick, June; Cock, David; Norrish, Michael

Description

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]

CollectionsANU Research Publications
Date published: 2009
Type: Conference paper
URI: http://hdl.handle.net/1885/23350
Source: Proceedings of International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009)
DOI: 10.1007/978-3-642-03359-9_34

Download

File Description SizeFormat Image
01_Winwood_Mind_the_Gap:_Verification_2009.pdf584.92 kBAdobe PDF    Request a copy
02_Winwood_Mind_the_Gap:_Verification_2009.pdf105.66 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  12 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator