Sciweavers

Share
FM
2009
Springer

Reasoning about Memory Layouts

9 years 9 months ago
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 arrays 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.
Holger Gast
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where FM
Authors Holger Gast
Comments (0)
books