Secure microkernels, state monads and scalable refinement
Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs …, 2008•Springer
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 …
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 …
Abstract
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.
Springer
