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.
@InProceedings{Klein_DE_09,
author = {Gerwin Klein and Philip Derrin and Kevin Elphinstone},
title = {Experience report: seL4 --- Formally Verifying a High-Performance Microkernel},
booktitle = {Proc.\ 2009 ACM SIGPLAN International Conference on Functional Programming (ICFP)},
year = {2009},
pages = {91--96},
month = Aug,
publisher = {ACM}
}