基于携带证明的代码的垃圾收集过程验证.pdf
时间:06-17 14:58
查看:612次
下载:163次
简介：
本文工作使用基于Hoare逻辑的汇编语言级形式程序验证框架，对垃圾收集
器的安全性和正确性，以及垃圾收集器与多种用户程序，特别是类型化汇编语言的交互过程的安全性进行了严格的形式验证。本文工作基于携带证明的代码技术，所有的验证都在计算机辅助定理证明工具CoQ中实现为计算机可检查的证明。这样，垃圾收集器和用户程序就能够被构造为一个完整的携带安全性明的软件包，方便地通过互联网和其他渠道进行发布。
畅学电子
