[isabelle] Types, Bytes, and Separation Logic



Hi all,

we are pleased to announce our paper

  Harvey Tuch, Gerwin Klein and Michael Norrish
  Types, Bytes, and Separation Logic. 
  In: M. Hofmann and M. Felleisen (eds), POPL'07. 
  12 pages, 2007, to appear. 

Abstract:
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.

URL:
  http://ertos.nicta.com.au/research/l4.verified/kmalloc.pml

Enjoy!
Gerwin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.