《表1 Coq文件和代码行数统计》
提示：宽带有限、当前游客访问压缩模式
本文基于一个已有的操作系统验证框架，在Coq中为SpaceOS内核建立了抽象模型，形式化定义了8条全局性质，给出了内核具有这些性质的机器可检查的证明.设计的全局性质推理规则扩展了已有的验证框架，连同开发的Coq证明策略一起为全局性质验证提供了更好的支持.这些扩展不仅提高了SpaceOS的验证效率，也有利于今后验证其他操作系统的全局性质.相关Coq文件和代码量统计如表1所示:
| 图表编号 | XD0045014700 严禁用于非法目的 |
|---|---|
| 绘制时间 | 2019.01.01 |
| 作者 | 顾海博、付明、乔磊、冯新宇 |
| 绘制单位 | 中国科学技术大学计算机科学与技术学院、中国科学技术大学苏州研究院软件安全实验室、中国科学技术大学苏州研究院软件安全实验室、华为上海研究所2012实验室-OS内核实验室、北京控制工程研究所、中国科学技术大学苏州研究院软件安全实验室、南京大学计算机软件新技术国家重点实验室 |
| 更多格式 | 高清、无水印（增值服务） |
