Types, Maps and Separation Logic

Select |




Print


Kolanski, Rafal; Klein, Gerwin

Kolanski, Rafal; Klein, Gerwin


2009-08-20


Conference Material


TPHOLs


Munich, Germany


276-292


This paper presents a separation-logic framework for reasoning 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 precise, 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.


Springer


Isabelle/HOL, Virtual Memory, seL4


http://www.springerlink.com/content/m853h8912641/?p=6c938061f299441bbb60953e185385ec&pi=72


nicta:1849


Kolanski, Rafal; Klein, Gerwin. Types, Maps and Separation Logic. In: S. Berghofer, T. Nipkow, C. Urban, M. Wenzel Editor, editor/s. TPHOLs; Munich, Germany. Springer; 2009-08-20. 276-292.



Loading citation data...

Citation counts
(Requires subscription to view)