Skip to main content


Mapped separation logic


Rafal Kolanski and Gerwin Klein




We present Mapped Separation Logic, an instance of Separation Logic for reasoning about virtual memory. Our logic is formalised in the Isabelle/HOL theorem and it allows reasoning on properties about page tables, direct physical memory access, virtual memory access, and shared memory. Mapped Separation Logic fully supports all rules of abstract Separation Logic, including the frame rule.

BibTeX Entry

    publisher        = {Springer},
    isbn             = {978-3-540-87872-8},
    author           = {Kolanski, Rafal and Klein, Gerwin},
    month            = oct,
    editor           = {{Natarajan Shankar, Jim Woodcock}},
    year             = {2008},
    keywords         = {isabelle, hol, virtual memory, separation logic},
    title            = {Mapped Separation Logic},
    booktitle        = {Verified Software: Theories, Tools and Experiments},
    pages            = {15-29},
    address          = {Toronto, Canada}


Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.