Skip to main content


Mechanised separation algebra


Gerwin Klein, Rafal Kolanski and Andrew Boyton




We present an Isabelle/HOL library with a generic type class implementation of separation algebra, develop basic separation logic concepts on top of it, and implement generic automated tactic support that can be used directly for any instantiation of the library. We show that the library is usable by multiple example instantiations that include common as well as more exotic base structures such as heap and virtual memory, and report on our experience using it in operating systems kernel verification.

BibTeX Entry

    publisher        = {Springer},
    author           = {Klein, Gerwin and Kolanski, Rafal and Boyton, Andrew},
    month            = aug,
    editor           = {{Lennart Beringer and Amy Felty}},
    year             = {2012},
    keywords         = {isabelle, separation logic},
    title            = {Mechanised Separation Algebra},
    booktitle        = {International Conference on Interactive Theorem Proving},
    pages            = {332-337},
    address          = {Princeton, USA}


Served by Apache on Linux on seL4.