Email Gateway (Aug 18 2022 at 10:01): Email Gateway (Aug 18 2022 at 10:01):From: Gerwin Klein <gerwin.klein@nicta.com.au>
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
Last updated: May 03 2024 at 04:19 UTC