We present a scalable, practical Hoare Logic and refinement calculus for the nondeterministic state monad with exceptions and failure in Isabelle/HOL. The emphasis of this formalisation is on large-scale verification of imperative-style functional programs, rather than expressing monad calculi in full generality. We achieve scalability in two dimensions. The method scales to multiple team members working productively and largely independently on a single proof and also to large programs with large and complex properties. We report on our experience in applying the techniques in an extensive (100,000 lines of proof) case study-the formal verification of an executable model of the seL4 operating system microkernel. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Cock, D., Klein, G., & Sewell, T. (2008). Secure microkernels, state monads and scalable refinement. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5170 LNCS, pp. 167–182). Springer Verlag. https://doi.org/10.1007/978-3-540-71067-7_16
Mendeley helps you to discover research relevant for your work.