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.
@InProceedings{Cock_KS_08,
author = {David Cock and Gerwin Klein and Thomas Sewell},
title = {Secure Microkernels, State Monads and Scalable Refinement},
booktitle = {Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs'08)},
year = {2008},
editor = {Otmane Ait Mohamed and C\'{e}sar Mu\~{n}oz and Sofi\`{e}ne Tahar},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
pages = {167--182},
volume = {5170},
}