Name
Abstract | ||
|---|---|---|
We present Mapped Separation Logic, an instance of Separa- tion Logic for reasoning about virtual memory. Our logic is formalised in the Isabelle/HOL theorem prover 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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-87873-5_6 | Verified Software: Theories, Tools, Experiments |
Keywords | Field | DocType |
virtual memory access,separation logic,direct physical memory access,hol theorem prover,shared memory,abstract separation logic,frame rule,virtual memory,mapped separation logic,page table,theorem prover | Separation logic,Programming language,Physical address,Computer science,Virtual memory,Multimodal logic,Description logic,Bunched logic,Theoretical computer science,Memory map,Distributed shared memory | Conference |
Volume | ISSN | Citations |
5295 | 0302-9743 | 3 |
PageRank | References | Authors |
0.45 | 12 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rafal Kolanski | 1 | 802 | 34.23 |
| Gerwin Klein | 2 | 1450 | 87.47 |