Local reasoning about a copying garbage collector

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

  • Lars Birkedal
  • Noah Torp-Smith, Copenhagen University Hospital, The Heart Centre, Copenhagen, Denmark
  • John C. Reynolds, Carnegie Mellon University, Denmark

We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We then state what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation logics [18, 23] to formally specify partial correctness of Cheney's copying garbage collector [8]. Finally, we prove that our implementation of Cheney's algorithm meets its specification, using the logic we have given, and auxiliary variables [19].

Original languageEnglish
JournalSIGPLAN Notices
Volume39
Issue1
Pages (from-to)220-231
Number of pages12
ISSN0362-1340
Publication statusPublished - 1 Jan 2004

Bibliographical note

Also publ. in: POPL '04 Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Pages 220-23.ACM

    Research areas

  • Copying garbage collector, Local reasoning, Separation logic

See relations at Aarhus University Citationformats

ID: 81614949