A Logic for Virtual Memory

Select |




Print


Kolanski, Rafal

Kolanski, Rafal


2008-07-21


Conference Material


3rd intl Workshop on Systems Software Verification (SSV08)


Sydney, Australia


61-77


We present an extension to classical separation logic which allows reasoning about virtual memory. Our logic is formalised in the Isabelle/HOL theorem prover in a manner allowing classical separation logic notation to be used at an abstract level. We demonstrate that in the common cases, such as user applications, our logic reduces to classical separation logic. At the same time we can express properties about page tables, direct physical memory access, virtual memory access, and shared memory in detail.


virtual memory separation logic


nicta:112


Kolanski, Rafal. A Logic for Virtual Memory. In: Ralf Huuck, Gerwin Klein, Bastian Schlich Editor, editor/s. 3rd intl Workshop on Systems Software Verification (SSV08); Sydney, Australia. 2008-07-21. 61-77.



Loading citation data...

Citation counts
(Requires subscription to view)