Types, Bytes, and Separation Logic

Select |




Print


Tuch, Harvey; Klein, Gerwin; Norrish, Michael

Tuch, Harvey; Klein, Gerwin; Norrish, Michael


2007-01-19


Conference Material


Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07)


Nice, France


97-108


We present a formal model of memory that both captures the low-level features of C's pointers and memory, and that forms the basis for an expressive implementation of separation logic. At the low level, we do not commit common oversimplifications, but correctly deal with C's model of programming language values and the heap. At the level of separation logic, we are still able to reason abstractly and efficiently. We implement this framework in the theorem prover Isabelle/HOL and demonstrate it on two case studies. We show that the divide between detailed and abstract does not impose undue verification overhead, and that simple programs remain easy to verify. We also show that the framework is applicable to real, security- and safety-critical code by formally verifying the memory allocator of the L4 microkernel.


ACM


Separation Logic, C, Interactive Theorem Proving, Isabelle


http://portal.acm.org/citation.cfm?id=1190234


1-59593-575-4


nicta:134


Tuch, Harvey; Klein, Gerwin; Norrish, Michael. Types, Bytes, and Separation Logic. In: Martin Hofmann and Matthias Felleisen Editor, editor/s. Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07); Nice, France. ACM; 2007-01-19. 97-108.



Loading citation data...

Citation counts
(Requires subscription to view)