seL4: formal verification of an operating-system kernel
By Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish and 3 more. Communications of the ACM, 2010
346 citations recorded by the source corpus.
Subfields: Computer Networks and Communications, Hardware and Architecture
View Paper: https://www.semanticscholar.org/paper/6f2641eda5c0aa20e6dfc7cb09c57735fe1b9222
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Computer Networks and Communications
- Josef Urban
- John Harrison
- Freek Wiedijk
- Alexander A. Alemi
- François Chollet
- Gernot Heiser
- Cezary Kaliszyk
- Niklas Eén
In Hardware and Architecture
Citations in the corpus
- History of Interactive Theorem Proving (2014, methodology): “Subsequently several other versions of HOL were written, including HOL Light, a version with a simplified axiomatization and rationalized structure written in CAML Light by one of the present authors and subsequently ported to OCaml [Harrison, 2006a], and Isabelle/HOL, described in more detail in th”
- DeepMath - Deep Sequence Models for Premise Selection (2016, methodology): “ITP verifications of the seL4 kernel [27] and CompCert compiler [29] show comparable progress in large scale software verification.”
- Comprehensive formal verification of an OS microkernel (2014, methodology): “In previous work [Klein et al. 2009b, 2010] we had concentrated on the functional correctness of seL4, which we later extended with binary veri.cation [Sewell et al. 2013] and the functional correctness veri.cation of seL4 s IPC fastpath described below in Section 4.6.”
- Deep Network Guided Proof Search (2017, background): “, 2015), or the proof of correctness of the seL4 operating system kernel (Klein et al., 2010).”