科研之友
微信
新浪微博
Facebook
分享链接
摘要
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.
- 出版日期2007-5
- 单位中国科学技术大学
