A Formal C Memory Model for Separation Logic

Robbert Krebbers

Research output: Contribution to journalArticleScientificpeer-review

4 Citations (Scopus)


The core of a formal semantics of an imperative programming language is a memory model that describes the behavior of operations on the memory. Defining a memory model that matches the description of C in the C11 standard is challenging because C allows both high-level (by means of typed expressions) and low-level (by means of bit manipulation) memory accesses. The C11 standard has restricted the interaction between these two levels to make more effective compiler optimizations possible, at the expense of making the memory model complicated. We describe a formal memory model of the (non-concurrent part of the) C11 standard that incorporates these restrictions, and at the same time describes low-level memory operations. This formal memory model includes a rich permission model to make it usable in separation logic and supports reasoning about program transformations. The memory model and essential properties of it have been fully formalized using the Coq proof assistant.
Original languageEnglish
Pages (from-to)319-387
Number of pages69
JournalJournal of Automated Reasoning
Issue number4
Publication statusPublished - 2016
Externally publishedYes


Dive into the research topics of 'A Formal C Memory Model for Separation Logic'. Together they form a unique fingerprint.

Cite this