Name
Abstract | ||
|---|---|---|
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.
|
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-03359-9_34 | Theorem Proving in Higher Order Logics |
Keywords | DocType | Volume |
Nature,science,science news,biology,physics,genetics,astronomy,astrophysics,quantum physics,evolution,evolutionary biology,geophysics,climate change,earth science,materials science,interdisciplinary science,science policy,medicine,systems biology,genomics,transcriptomics,palaeobiology,ecology,molecular biology,cancer,immunology,pharmacology,development,developmental biology,structural biology,biochemistry,bioinformatics,computational biology,nanotechnology,proteomics,metabolomics,biotechnology,drug discovery,environmental science,life,marine biology,medical research,neuroscience,neurobiology,functional genomics,molecular interactions,RNA,DNA,cell cycle,signal transduction,cell signalling | Conference | 454 |
Issue | ISSN | Citations |
7203 | 1476-4687 | 0 |
PageRank | References | Authors |
0.34 | 6 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Simon Winwood | 1 | 713 | 30.07 |
| Gerwin Klein | 2 | 1450 | 87.47 |
| Thomas Sewell | 3 | 914 | 37.60 |
| June Andronick | 4 | 903 | 42.66 |
| David Cock | 5 | 827 | 37.44 |
| Michael Norrish | 6 | 1091 | 61.77 |