Sciweavers

ICFP
2009
ACM
14 years 5 months ago
Experience report: seL4: formally verifying a high-performance microkernel
We report on our experience using Haskell as an executable specification language in the formal verification of the seL4 microkernel. fication connects an abstract operational spe...
Gerwin Klein, Philip Derrin, Kevin Elphinstone