Trustworthy Systems

Mapped separation logic

Authors

Rafal Kolanski and Gerwin Klein

NICTA

UNSW

Abstract

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

  @inproceedings{Kolanski_Klein_08,
    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         = {https://trustworthy.systems/publications/nicta_full_text/705.pdf},
    publisher        = {Springer},
    title            = {Mapped Separation Logic},
    year             = {2008}
  }

Download