Chris Hawblitzel ; Erez Petrank - Automated Verification of Practical Garbage Collectors

lmcs:1039 - Logical Methods in Computer Science, August 18, 2010, Volume 6, Issue 3 - https://doi.org/10.2168/LMCS-6(3:6)2010
Automated Verification of Practical Garbage Collectors

Authors: Chris Hawblitzel ; Erez Petrank

    Garbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graphs. Several papers have presented verified collectors, but either the proofs were hand-written or the collectors were too simplistic to use on practical applications. In this work, we present two mechanically verified garbage collectors, both practical enough to use for real-world C# benchmarks. The collectors and their associated allocators consist of x86 assembly language instructions and macro instructions, annotated with preconditions, postconditions, invariants, and assertions. We used the Boogie verification generator and the Z3 automated theorem prover to verify this assembly language code mechanically. We provide measurements comparing the performance of the verified collector with that of the standard Bartok collectors on off-the-shelf C# benchmarks, demonstrating their competitiveness.


    Volume: Volume 6, Issue 3
    Published on: August 18, 2010
    Accepted on: June 25, 2015
    Submitted on: October 13, 2009
    Keywords: Computer Science - Programming Languages

    Linked data

    Source : ScholeXplorer References DOI 10.1093/logcom/13.6.815
    • 10.1093/logcom/13.6.815
    Formal Verification of an Incremental Garbage Collector
    Solange Coupet-Grimal ; Catherine Nouvet ;

    5 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 370 times.
    This article's PDF has been downloaded 249 times.