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-Smith
John C. Reynolds

July 2003

Abstract

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.