| 渐进式标记-清扫垃圾收集机制验证 |
| |
| 引用本文： | 李隆,陈意云,林春晓.渐进式标记-清扫垃圾收集机制验证[J].小型微型计算机系统,2009,30(9). |
| |
| 作者姓名： | 李隆 陈意云 林春晓 |
| |
| 作者单位： | 中国科学技术大学计算机科学技术系,安徽,合肥,230026;中国科学技术大学苏州研究院软件安全实验室,江苏苏州,215123 |
| |
| 基金项目： | 国家自然科学基金项目，Intel中国研究中心资助 |
| |
| 摘 要： | 垃圾收集已经成为可靠、高效程序运行平台的一个重要组成部分.渐进式垃圾收集由于在用户程序运行时并行的执行垃圾收集操作,其算法及实现则更为复杂,其可靠性也更难以得到保证.本文论述使用Hoare风格的程序验证框架形式验证渐进式标记-清扫垃圾收集机制及其写拦截器在汇编语言层次上的实现的研究工作.被验证的属性涵括了简单的类型安全到整个内存堆上的数据保持.本文所有的验证工作都实现在Coq辅助定理证明工具中,从而可以迅速的用于构造携带证明的代码包.
|
| 关 键 词： | 软件安全 程序验证 垃圾收集 携带证明的代码 |
Verification of Incremental Mark-Sweep Garbage Collection |
| |
| LI Long,CHEN Yi-yun,LIN Chun-xiao.Verification of Incremental Mark-Sweep Garbage Collection[J].Mini-micro Systems,2009,30(9). |
| |
| Authors: | LI Long CHEN Yi-yun LIN Chun-xiao |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
