北京广利核系统工程有限公司 谷伟卿，张智慧，白涛，齐敏

摘要：同步数据流语言是一种广泛应用于核电及其他安全关键领域的语言，在同步数据流语言到顺序执行语言的翻译转换过程中，语义等价要保证赋值语句的左右值地址互不相交，这至关重要。本文使用形式化方法描述了翻译过程中地址互不相交的性质，并通过定理证明的方式对其进行了验证。基于本方法的编译器在某核电站的安全保护系统中得到了应用。

关键词：同步数据流；定理证明；Coq；语义等价；地址不相交

在线预览：可信编译器中地址不相交的保持性证明

摘自《自动化博览》2017年4月刊