Verification of the L4 kernel memory allocator

This page contains the proof document and the Isabelle/HOL scripts together with the code and invariants for the formal verification of the L4 kernel memory allocator.

The proof and separation logic framework it is using are explained in:

plain text PDF Harvey Tuch, Gerwin Klein and Michael Norrish
Types, bytes, and separation logic
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007

The following files are available:

  • [Proof document] This pdf document contains the code, invariants, and full proof scripts used in the paper (more recent document with stronger specifications).
  • [Bitvector library] This package contains a library for fixed length machine words in Isabelle/HOL. This is still in heavy development and provided as is.
  • [Unified memory model and separation logic]. These are the framework theories presented in the paper. The package requires the bitvector library mentioned above and the latest version of Norbert Schirmer's verification environment to build.
All Isabelle/HOL theories scripts are tested with the Isabelle development snapshot Isabelle_13-Nov-2006.