Formal Derivation of Concurrent Garbage Collectors

Dusko Pavlovic, Peter Pepper, Douglas R. Smith

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    21 Citations (Scopus)


    Concurrent garbage collectors are notoriously difficult to implement correctly. Previous approaches to the issue of producing correct collectors have mainly been based on posit-and-prove verification or on the application of domain-specific templates and transformations. We show how to derive the upper reaches of a family of concurrent garbage collectors by refinement from a formal specification, emphasizing the application of domain-independent design theories and transformations. A key contribution is an extension to the classical lattice-theoretic fixpoint theorems to account for the dynamics of concurrent mutation and collection.
    Original languageEnglish
    Title of host publicationMathematics of Program Construction
    Subtitle of host publication10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings
    EditorsClaude Bolduc, Jules Desharnais, Béchir Ktari
    Place of PublicationBerlin, Heidelberg
    Number of pages24
    ISBN (Electronic)978-3-642-13321-3
    ISBN (Print)978-3-642-13320-6
    Publication statusPublished - Jun 2010
    Event10th International Conference on Mathematics of Program Construction, MPC 2010 - Québec City, Canada
    Duration: 21 Jun 201023 Jun 2010
    Conference number: 10

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference10th International Conference on Mathematics of Program Construction, MPC 2010
    Abbreviated titleMPC
    CityQuébec City


    • Garbage collection
    • Formal derivation
    • Abstract problem
    • Live node
    • Garbage collector


    Dive into the research topics of 'Formal Derivation of Concurrent Garbage Collectors'. Together they form a unique fingerprint.

    Cite this