Local Reasoning about a Copying Garbage Collector

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

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer 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
    TidsskriftACM Transactions on Programming Languages and Systems
    Udgave nummer4
    Sider (fra-til)24-81
    Antal sider58
    StatusUdgivet - 2008