%0 Journal Article
%T Garbage Collector Verification for Proof-Carrying Code
%A Chun-Xiao Lin
%A Yi-Yun Chen
%A Long Li
%A Bei Hua
%A <br>Chun-Xiao Lin
%A Yi-Yun Chen
%A Long Li
%A and Bei Hua
%J 计算机科学技术学报
%D 2007
%I 
%X 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.
%K program verification
%K garbage collector
%K proof-carrying code
%K program safety<br>程序验证
%K 垃圾信息收集器
%K 程序安全
%K 证明携带码
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=F57FEF5FAEE544283F43708D560ABF1B&aid=CBCDFFE5AEBDB1BF606F24FD56BE9562&yid=A732AF04DDA03BB3&vid=BC12EA701C895178&iid=38B194292C032A66&sid=BA48F0B914ED890A&eid=B40AD8FE6FA88DE9&journal_id=1000-9000&journal_name=计算机科学技术学报&referenced_num=2&reference_num=25