TY - RPRT
T1 - Correctness of a Garbage Collector via Local Reasoning
AU - Birkedal, Lars
AU - Torp-Smith, Noah
AU - Reynolds, John C.
PY - 2003/7
Y1 - 2003/7
N2 - 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.
AB - 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.
M3 - Report
T3 - IT University Technical Report Series
BT - Correctness of a Garbage Collector via Local Reasoning
PB - IT-Universitetet i København
CY - Copenhagen
ER -