中文摘要：

垃圾收集已经成为可靠、高效程序运行平台的一个重要组成部分．渐进式垃圾收集由于在用户程序运行时并行的执行垃圾收集操作，其算法及实现则更为复杂，其可靠性也更难以得到保证．本文论述使用Hoare风格的程序验证框架形式验证渐进式标记-清扫垃圾收集机制及其写拦截器在汇编语言层次上的实现的研究工作．被验证的属性涵括了简单的类型安全到整个内存堆上的数据保持．本文所有的验证工作都实现在Coq辅助定理证明工具中，从而可以迅速的用于构造携带证明的代码包．

英文摘要：

Garbage collection has been an important component of efficient and reliable program execution platforms. The algorithm and implementation of incremental garbage collection have been more complicated because it collects garbage in parallel to user programs. And it is difficult to guarantee the reliability of incremental garbage collection. In this paper, we present the formal verification of the assembly-level implementation of incremental mark-sweep garbage collectors and write barriers in a Hoare-style program logic. The properties verified about the garbage collectors range from simple type safety to full heap preservation. And all of the verification is mechanized in the Coq proof assistant and can be used to pack as proof-carrying code packages immediately.