Local Reasoning about a Copying Garbage Collector

Lars Birkedal (The IT University of Copenhagen) Noah Torp-Smith (The IT University of Copenhagen) John C. Reynolds (Carnegie Mellon University)

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We then state what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation logicsto formally specify partial correctness of Cheney's copying garbage collector. Finally, we prove that our implementation of Cheney's algorithm meets its specification, using thelogic we have given, and auxiliary variables.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems