可信编译器中地址不相交的保持性证明

• 作者: 张智慧 白涛 谷伟卿 齐敏
• 来源期刊: 自动化博览
• 关键词: 同步数据流 定理证明 Coq 语义等价 地址不相交
• 年，卷（期）: 2017,（4）
• 所属期刊栏目: 核电仪控
• 页码范围: 72-78
• 页数: 7页
• 字数: 5945字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	白涛		8	23	3.0	4.0
2	齐敏		11	20	3.0	4.0
3	张智慧		5	8	2.0	2.0
4	谷伟卿		1	0	0.0	0.0