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