Local Reasoning about a Copying Garbage Collector

Noah Torp-Smith, Lars Birkedal, John C. Reynolds

    Research output: Journal Article or Conference Article in JournalJournal 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
    JournalACM Transactions on Programming Languages and Systems
    Issue number4
    Pages (from-to)24-81
    Number of pages58
    Publication statusPublished - 2008

    Cite this