Trustworthy Systems

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

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