期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到6篇文章
< 1 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
可信编译器构造的翻译确认方法简述 被引量：2
1
作者 刘洋 杨斐 +3 位作者 石刚 闫鑫 王生原 董渊 《计算机科学》 CSCD 北大核心 2014年第S1期334-338,共5页
编译器的安全可信问题日益引起重视,特别是在安全关键系统中,编译器的误编译将会造成重大的损失。消除误编译的传统方法是大量的测试,但是测试难以达到完全覆盖,并不能充分地保证编译器的安全可信。近年来,形式化验证方法被成功用于可... 编译器的安全可信问题日益引起重视,特别是在安全关键系统中,编译器的误编译将会造成重大的损失。消除误编译的传统方法是大量的测试,但是测试难以达到完全覆盖,并不能充分地保证编译器的安全可信。近年来,形式化验证方法被成功用于可信编译器的构造中。一种方法是对编译器本身进行形式化验证,经过严密的证明,可杜绝误编译的发生。然而,这种方法可能"冻结"编译器的设计,阻碍编译器未来可能的优化和完善。翻译确认是另外一种用于可信编译器构造的形式化方法,它避免了对编译器自身的验证,有很好的可重用性,近年来在编译器验证领域得到了广泛研究,已取得令人瞩目的成果。介绍了翻译确认方法的概念及研究进展。 展开更多
关键词 可信编译器 形式化验证方法 翻译确认 确认器
在线阅读 下载PDF
一种适用于可信编译器的源语言转换与检查框架 被引量：1
2
作者 张晓曈 何炎祥 《中国科技论文》 北大核心 2017年第14期1646-1650,共5页
针对当前可信编译器对源语言处理能力的局限,提出了1个适于可信编译器的源语言转换与检查框架,将命令式源语言程序转换为可信编译器可接受的等价的函数式语言程序,通过语法支持、良构性和异常发生三方面的检查,保证了可信编译器对转换... 针对当前可信编译器对源语言处理能力的局限,提出了1个适于可信编译器的源语言转换与检查框架,将命令式源语言程序转换为可信编译器可接受的等价的函数式语言程序,通过语法支持、良构性和异常发生三方面的检查,保证了可信编译器对转换后的代码的可接受性以及代码本身较高的可信性。 展开更多
关键词 编译验证 可信编译器 代码转换 操作语义
在线阅读 下载PDF
可信编译理论及其核心实现技术:研究综述 被引量：12
3
作者 何炎祥 吴伟 +5 位作者 刘陶 李清安 陈勇 胡明昊 刘健博 石谦 《计算机科学与探索》 CSCD 2011年第1期1-22,共22页
编译器是重要的系统软件之一,高级语言编写的软件都必须经过编译器的编译才能成为可执行程序。编译器的可信性对于整个计算机系统而言具有非常关键的意义,如果编译器不可信,则很难保证系统所运行软件的可信性。可信编译是指编译器在保... 编译器是重要的系统软件之一,高级语言编写的软件都必须经过编译器的编译才能成为可执行程序。编译器的可信性对于整个计算机系统而言具有非常关键的意义,如果编译器不可信,则很难保证系统所运行软件的可信性。可信编译是指编译器在保证编译正确的同时提供相应的机制保证编译对象的可信性,对可信编译理论和技术的研究具有重要理论意义和实用前景。阐述了可信编译器的概念,介绍了编译过程正确性的形式化定义,对可信编译的主要研究进行了概括。在全面分析可信编译研究现状的基础上,从编译器自身可信性和确保编译对象可信性两个方面,对可信编译器设计和实现的相关理论和方法进行了分类和总结。最后,讨论了可信编译有待解决的问题和未来的研究方向。 展开更多
关键词 可信编译器 编译正确性 编译器验证 可信软件
在线阅读 下载PDF
同步数据流语言时态消去的可信翻译 被引量：5
4
作者 张玲波 甘元科 +4 位作者 石刚 王生原 董渊 张智慧 王沿海 《计算机工程与设计》 CSCD 北大核心 2014年第1期137-143,共7页
为解决实现同步数据流语言Lustre到串行命令式语言C语言可信编译器过程中碰到的时态运算翻译的困难,提出了将所有的时态运算翻译单独分层定义和证明的方法。在同步数据流语言的时态特性和C语言的循环特性分析的基础上,结合可信编译器实... 为解决实现同步数据流语言Lustre到串行命令式语言C语言可信编译器过程中碰到的时态运算翻译的困难,提出了将所有的时态运算翻译单独分层定义和证明的方法。在同步数据流语言的时态特性和C语言的循环特性分析的基础上,结合可信编译器实现框架上下层的语言结构,使用Coq证明工具,形式化的定义了两种中间语言的语法和语义,经过分析时态翻译过程特点,归纳定义了时态变量传递性质,实现了翻译工作严格的形式化验证,最终完成了时态消去翻译的等价性证明。 展开更多
关键词 同步数据流语言 可信编译器 形式化验证 时态消去 COQ
在线阅读 下载PDF
同步数据流语言pre算子在Coq中的翻译验证
5
作者 李春燕 赵长名 +2 位作者 杨斐 马权 侯荣彬 《西华大学学报(自然科学版)》 2025年第2期87-95,共9页
文章对同步数据流语言的pre算子进行详细处理,除了将pre算子翻译至fby算子,还对pre算子在第一周期的值根据其输入参数类型的不同做了相应的初始化,解决了pre算子第一周期为空的问题。输入参数为整型和布尔型,其第一周期初始化为false,... 文章对同步数据流语言的pre算子进行详细处理,除了将pre算子翻译至fby算子,还对pre算子在第一周期的值根据其输入参数类型的不同做了相应的初始化,解决了pre算子第一周期为空的问题。输入参数为整型和布尔型,其第一周期初始化为false,浮点型初始化为浮点零;数组和结构体类型,根据其元素类型分别进行不同的初始化。由于pre算子的翻译应用场景大多在核电安全级数字化控制系统(SDCS),因此为了确保其编译的正确性及安全性,整个翻译过程在辅助定理证明器Coq完成了形式化验证。同时该翻译及验证方法在SDCS中进行试用,达到了预期的翻译效果。 展开更多
关键词 同步数据流语言 可信编译器 形式化验证
在线阅读 下载PDF
同步数据流语言输入结构体的可信翻译
6
作者 刘莛杨 吴锡 +4 位作者 杨斐 侯荣彬 马权 王汝桥 梁根华 《计算机系统应用》 2023年第6期269-277,共9页
为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉... 为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范. 展开更多
关键词 同步数据流语言 形式化验证 仪控系统 可信编译器
在线阅读 下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
使用帮助 返回顶部