同步数据流语言高阶运算消去的可信翻译?

• 作者: 刘洋 杨斐 王生原 甘元科 石刚 董渊 闫鑫
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 同步数据流语言 形式化验证 高阶运算 定理证明
• 年，卷（期）: 2015,（2）
• 页码范围: 332-347
• 页数: 16页
• 分类号: TP314
• 字数: 10840字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004785

摘要

Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言，采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度。基于这种方法，开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究。由于Lustre*与Clight之间巨大的语言差异，整个编译过程划分为多个层次，每个层次完成特定的翻译工作。阐述了其中高阶运算消去的翻译算法，翻译过程采用辅助定理证明工具Coq实现，并进行严格的正确性证明。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	石刚	清华大学计算机科学与技术系	9	15	2.0	3.0
3	董渊	清华大学计算机科学与技术系	33	386	10.0	18.0
4	王生原	清华大学计算机科学与技术系	33	235	8.0	14.0
5	刘洋	清华大学计算机科学与技术系	71	308	9.0	16.0
8	杨斐	清华大学计算机科学与技术系	3	10	2.0	3.0
9	甘元科	清华大学计算机科学与技术系	5	24	4.0	4.0