Types, bytes, and separation logic

Harvey Tuch*, Gerwin Klein, Michael Norrish

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

59 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationConference Record of POPL 2007
Subtitle of host publicationThe 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Papers Presented at the Symposium
Pages97-108
Number of pages12
DOIs
Publication statusPublished - 2007
Externally publishedYes
Event34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Nice, France
Duration: 17 Jan 200719 Jan 2007

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Conference

Conference34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Country/TerritoryFrance
CityNice
Period17/01/0719/01/07

Fingerprint

Dive into the research topics of 'Types, bytes, and separation logic'. Together they form a unique fingerprint.

Cite this