A Logic for Virtual Memory
The work
| Authors | Rafal Kolanski |
|---|---|
| Editors | |
| Type | article |
| Year | 2008 |
| Citekey | kolanski2008logic |
Where it appeared
| Published in | Electronic Notes in Theoretical Computer Science |
|---|---|
| Publisher | Elsevier BV |
| Volume | 217 |
| Pages | 61--77 |
Identifiers
| DOI | 10.1016/j.entcs.2008.06.042 |
|---|---|
| OpenAlex | W2070525984 |
Access
| Landing page | https://doi.org/10.1016/j.entcs.2008.06.042 |
|---|---|
| Free full text | https://www.sciencedirect.com/science/article/pii/S157106610800385X/pdf |
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
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.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 14:20 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{kolanski2008logic,
title = {A Logic for Virtual Memory},
author = {Rafal Kolanski},
year = {2008},
journal = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier BV},
volume = {217},
pages = {61--77},
doi = {10.1016/j.entcs.2008.06.042},
}
This record lives at https://refs.drheap.org/kolanski2008logic/ and will keep doing so.