Name
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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1016/j.entcs.2008.06.042 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
virtual memory access,abstract level,hol theorem prover,interactive theorem proving,shared memory,virtual memory,common case,separation logic,direct physical memory access,classical separation logic,classical separation logic notation,page table,theorem prover | Separation logic,Uniform memory access,Programming language,Computer science,Virtual memory,Multimodal logic,Theoretical computer science,Bunched logic,Memory map,Distributed shared memory,Dynamic logic (modal logic) | Journal |
Volume | ISSN | Citations |
217, | Electronic Notes in Theoretical Computer Science | 4 |
PageRank | References | Authors |
0.46 | 10 | 1 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rafal Kolanski | 1 | 802 | 34.23 |