Output details
11 - Computer Science and Informatics
University of Cambridge
Output title
Translation Validation for a Verified OS Kernel
Type
E - Conference contribution
Name of conference/published proceedings
PLDI: 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation
Volume number
-
Issue number
-
First page of article
N/A
ISSN of proceedings
-
Year of publication
2013
Number of additional authors
2
Additional information
<07> This paper, described as "a tour de force of formal verification" by
John Regehr (a systems programmer) on his famous blog on 21 May
2012, shows that the methods that I developed during my PhD (my
thesis was selected as the winner of the British Computer Society's
Distinguished Dissertation Competition 2010) scale to significant
case studies. In this case, to a fully featured operating system kernel,
the seL4 microkernel. Together with Thomas Sewell, I verified the
correctness of the binary that GCC produces from the C code for
the kernel.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
-
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
