Reasoning about memory layouts
Verification methods for memory-manipulating C programs need to address not only well-typed programs that respect invariants
such as the split-heap memory model, but also programs that access through pointers arbitrary memory objects such as local
variables, single struct fields, or array slices. We present a logic for memory layouts that covers these applications and
show how proof obligations arising during the verification can be discharged automatically using the layouts. The framework
developed in this way is also suitable for reasoning about data structures manipulated by algorithms, which we demonstrate
by verifying the Schorr-Waite graph marking algorithm.