Experience report: seL4: formally verifying a high-performance microkernel Export

@inproceedings{citeulike:5724338, abstract = {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.}, address = {New York, NY, USA}, author = {Klein, Gerwin and Derrin, Philip and Elphinstone, Kevin}, booktitle = {ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming}, citeulike-article-id = {5724338}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1596550.1596566}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1596550.1596566}, doi = {10.1145/1596550.1596566}, isbn = {978-1-60558-332-7}, keywords = {formal-proof, isabelle, language-haskell, operating-system, os-sel4}, location = {Edinburgh, Scotland}, pages = {91--96}, posted-at = {2009-09-04 18:45:42}, priority = {0}, publisher = {ACM}, title = {Experience report: seL4: formally verifying a high-performance microkernel}, url = {http://dx.doi.org/10.1145/1596550.1596566}, year = {2009} }

TY - CONF ID - citeulike:5724338 L3 - citeulike-article-id:5724338 N2 - 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. CY - Edinburgh, Scotland SN - 978-1-60558-332-7 AD - New York, NY, USA EP - 96 TI - Experience report: seL4: formally verifying a high-performance microkernel PB - ACM T2 - ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming SP - 91 KW - formal-proof KW - isabelle KW - language-haskell KW - operating-system KW - os-sel4 AU - Klein, Gerwin AU - Derrin, Philip AU - Elphinstone, Kevin PY - 2009/// UR - http://dx.doi.org/10.1145/1596550.1596566 ER -