Garbage Collector Verification for Proof-Carrying Code

We present the verification of the machine-level implementation of a conservative variant of the standard mark-sweep garbage collector in a Hoare-style program logic. The specification of the collector is given on a machine-level memory model using separation logic, and is strong enough to preserve...

Full description

Saved in:
Bibliographic Details
Published in:Journal of computer science and technology 2007-05, Vol.22 (3), p.426-437
Main Authors: Lin, Chun-Xiao, Chen, Yi-Yun, Li, Long, Hua, Bei
Format: Article
Language:English
Subjects:
Accumulators
Collectors
Garbage
Logic
Packages
Preserves
Specifications
Verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present the verification of the machine-level implementation of a conservative variant of the standard mark-sweep garbage collector in a Hoare-style program logic. The specification of the collector is given on a machine-level memory model using separation logic, and is strong enough to preserve the safety property of any common mutator program. Our verification is fully implemented in the Coq proof assistant and can be packed immediately as foundational proof-carrying code package. Our work makes important attempt toward building fully certified production-quality garbage collectors.
ISSN:1000-9000
1860-4749
DOI:10.1007/s11390-007-9049-z