Name
Abstract | ||
|---|---|---|
This paper presents a separation-logic framework for reason- ing about low-level C code in the presence of virtual memory. We describe our abstract, generic Isabelle/HOL framework for reasoning about virtual memory in separation logic, and we instantiate this framework to a pre- cise, formal model of ARMv6 page tables. The logic supports the usual separation logic rules, including the frame rule, and extends separation logic with additional basic predicates for mapping virtual to physical addresses. We build on earlier work to parse potentially type-unsafe, system-level C code directly into Isabelle/HOL and further instantiate the separation logic framework to C. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-03359-9_20 | Theorem Proving in Higher Order Logics |
Keywords | Field | DocType |
separation logic,generic isabelle,hol framework,usual separation logic rule,low-level c code,virtual memory,separation logic framework,system-level c code,armv6 page table,separation-logic framework | Computational logic,Separation logic,Autoepistemic logic,Programming language,Computer science,Algorithm,Multimodal logic,Description logic,Theoretical computer science,Bunched logic,Dynamic logic (modal logic),Higher-order logic | Conference |
Volume | ISSN | Citations |
5674 | 0302-9743 | 4 |
PageRank | References | Authors |
0.78 | 12 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rafal Kolanski | 1 | 802 | 34.23 |
| Gerwin Klein | 2 | 1450 | 87.47 |