Experience Report: seL4 -- Formally Verifying a High-Performance Microkernel

Select |




Print


Klein, Gerwin; Derrin, Philip; Elphinstone, Kevin

Klein, Gerwin; Derrin, Philip; Elphinstone, Kevin


2009-08-31


Conference Material


ICFP


Edinburgh, UK


91-96


We report on our experience using Haskell as an executable specification language in the formal verification of the seL4 microkernel. The verification connects an abstract operational specification in the theorem prover Isabelle/HOL to a C implementation of the microkernel. We describe how this project differs from other efforts, and examine the effect of using Haskell in a large-scale formal verification. The kernel comprises 8,700 lines of C code; the verification more than 150,000 lines of proof script.


ACM


seL4, microkernel, Isabelle, formal verification


http://portal.acm.org/citation.cfm?id=1596550.1596566&coll=portal&dl=ACM&type=series&idx=SERIES824&part=series&WantType=Proceedings&title=ICFP&CFID=505049525&CFTOKEN=505049525


nicta:1817


Klein, Gerwin; Derrin, Philip; Elphinstone, Kevin. Experience Report: seL4 -- Formally Verifying a High-Performance Microkernel. In: Andrew Tolmach Editor, editor/s. ICFP; Edinburgh, UK. ACM; 2009-08-31. 91-96.



Loading citation data...

Citation counts
(Requires subscription to view)