Translation validation for a verified OS kernel

PLDI, pp. 471-482, 2013.

Cited by: 84|Views21
EI

Abstract:

We extend the existing formal verification of the seL4 operating system microkernel from 9500 lines of C source code to the binary level. We handle all functions that were part of the previous verification. Like the original verification, we currently omit the assembly routines and volatile accesses used to control system hardware. More g...More

Code:

Data:

Your rating :
0

 

Tags
Comments