@book{8540e7d1ea054c13b305022fe1af5b65,
title = "Correctness of a Garbage Collector via Local Reasoning",
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.",
keywords = "programming language, memory management, copying garbage collector, Separation Logic, formal specification",
author = "Lars Birkedal and Noah Torp-Smith and Reynolds, \{John C.\}",
year = "2003",
month = jul,
language = "English",
series = "IT University Technical Report Series",
number = "TR-2003-30",
publisher = "IT-Universitetet i K{\o}benhavn",
address = "Denmark",
edition = "TR-2003-30",
}