核安全级控制算法描述语言的可信编译研究

摘要：

本文主要讲述核安全级控制算法描述语言Lustre 编译器ACG 的开发和形式化验证(语 义保持性证明)，该编译器将图形化的Lustre 程序编译为行为等价的C 代码，用定理证明辅助工 具Coq 来开发编译器并证明其正确性。在关注安全关键软件及其形式化验证的环境中，这种经 过验证的编译器是极其重要的：编译器的验证可保证，源代码中已证明的安全性质能够在编译产 生的目标代码里继续得到保持。

关键词： 编译器 形式化验证 定理证明 Coq ACG R2L L2C

作者: 张智慧 齐敏 冀建伟 王沿海

作者单位: 北京广利核系统工程有限公司,北京市海淀区永丰路5号院5号楼,100094

会议类型: 国内会议

会议名称: 第一届中国(国际)核电仪控技术大会

会议地点: 北京

会议语种:中文

页码: 518-525

在线出版日期: 2011-05-26（万方平台首次上网日期，不代表论文的发表时间）