3. Week 03: Reasoning about Heap-Manipulating Programs

3.1. Mandatory Reading

• Pointers and Data Structures: Separation Logic (by Xavier Leroy)

3.2. Accompanying Code

• Separation Logic in Coq

3.3. Recommended Reading

• John C. Reynolds: Separation Logic: A Logic for Shared Mutable Data Structures, 2002
• Peter W. O’Hearn: A Primer on Separation Logic, 2012