Klein, GerwinElphinstone, KevinHeiser, GernotAndronick, JuneCock, DavidDerrin, PhilipElkaduwe, DhammikaEngelhardt, KaiKolanski, RafalNorrish, MichaelSewell, ThomasTuch, HarveyWinwood, Simon2015-12-07October 119781605587523http://hdl.handle.net/1885/23164Keywords: Abstract specifications; Assembly code; C codes; Design approaches; Formal proofs; Formal verifications; Isabelle/HOl; Operating systems; Programming errors; Safety property; System kernel; Third generation; Computer operating systems; Specifications; Abs Isabelle/HOL; L4; Microkernel; seL4seL4: Formal Verification of an OS Kernel200910.1145/1629575.16295962016-06-14