Structured Types and Separation Logic

Structured types, such as C's arrays and structs, present additional challenges in pointer program verification. The conventional proof abstractions, multiple independent typed heaps and separation logic, which in previous work have been built on a low-level memory model for C and shown to be sound, are not directly applicable in verifications. This is due to the non-monotonic nature of pointer and lvalue validity in the presence of the unary &-operator. For example, type-safe updates through pointers to fields of a struct break the independence of updates across typed heaps or ∧∗-conjuncts. In this paper we present a generalisation of our earlier formal memory model that captured the low-level features of C's pointers and memory and formed the basis for an expressive implementation of separation logic, with new features providing explicit support for C's structured types. We implement this framework in the theorem prover Isabelle/HOL and all proofs are machine checked.