Correctness of a Garbage Collector via Local Reasoning
TR-2003-30, Author: Lars Birkedal, Noah Torp-Smith and John C. Reynolds Lars Birkedal Noah Torp-Smit
h John C. Reynolds
We give a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We then outline what is meant by correctness of a copying garbage collector, and employ a variant of the novel Separation Logics to formally specify correctness. We then prove that our implementation meets its specification, using the logic we have given, and auxiliary variables.
Technical report TR-2003-30 in IT University Technical Report Series, July 2003.
Available as PDF