Comparing Heap Models: Ownership, Dynamic Frames, Permissions - Leino, Rustan (Typing, Analysis and Verification of Heap-Manipulating Programs, Dagstuhl, Germany, 2009)
Specification challenges Invariants Describes what holds of an object in its steady state When does an invariant hold? Frames Describes what is being modified or read Goals Flexibility Conciseness