Aarhus University Seal / Aarhus Universitets segl

Local Reasoning about a Copying Garbage Collector

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

We present a programming language, model, and logic appropriate for implementing and reasoning
about a memory management system. We state semantically what is meant by correctness of a
copying garbage collector, and employ a variant of the novel separation logics to formally specify
partial correctness of Cheney’s copying garbage collector in our program logic. Finally, we prove
that our implementation of Cheney’s algorithm meets its specification using the logic we have given
and auxiliary variables.
Udgivelsesdato: 2008
Original languageEnglish
JournalA C M Transactions on Programming Languages and Systems
Pages (from-to)24-81
Number of pages58
Publication statusPublished - 2008
Externally publishedYes

See relations at Aarhus University Citationformats

ID: 73743521