Reasoning about memory layouts

Reasoning about memory layouts,10.1007/s10703-010-0098-5,Formal Methods in System Design,Holger Gast

Reasoning about memory layouts  
BibTex | RIS | RefWorks Download
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.
Journal: Formal Methods in System Design - FMSD , vol. 37, no. 2-3, pp. 141-170, 2010
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.