Types, bytes, and separation logic

13 years 10 months ago
Types, bytes, and separation logic
We present a formal model of memory that both captures the lowlevel 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. evel 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 de 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. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs--Mechanical verification General Terms Languages, The...
Harvey Tuch, Gerwin Klein, Michael Norrish
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where POPL
Authors Harvey Tuch, Gerwin Klein, Michael Norrish
Comments (0)