Garbage Collector Verification for Proof-Carrying Code

We present the verification of themachine-level implementation of a conservative variant of the standardmark-sweep garbage collector in a Hoare-style program logic. Thespecification of the collector is given on a machine-level memory modelusing separation logic, and is strong enough to preserve the safetyproperty of any common mutator program. Our verification is fullyimplemented in the Coq proof assistant and can be packed immediately asfoundational proof-carrying code package. Our work makes importantattempt toward building fully certified production-quality garbagecollectors.