Trustworthy Systems

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

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