首页 | 本学科首页   官方微博 | 高级检索  
检索     
共有20条相似文献,以下是第1-20项 搜索用时 187 毫秒

1.  可信编译器L2C的核心翻译步骤及其设计与实现  
   尚书  甘元科  石刚  王生原  董渊《软件学报》,2017年第28卷第5期
   同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好”误编译”问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证取得了很大的成功,如CompCert C编译器.L2C是基于这种方法开发的可信编译器,它以扩展的Lustre语言为源语言,以Clight (CompCert中的C语言子集)为目标语言.就我们所知,L2C是同类工作中唯一面向实际工业应用的同步数据流语言编译器.本文重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.    

2.  同步数据流语言高阶运算消去的可信翻译  
   刘洋  甘元科  王生原  董渊  杨斐  石刚  闫鑫《软件学报》,2015年第26卷第2期
   Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言,采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度.基于这种方法,开展了从Lustre*(一种类Lustre语言)到C子集Clight的可信编译器的研究.由于Lustre*与Clight之间巨大的语言差异,整个编译过程划分为多个层次,每个层次完成特定的翻译工作.阐述了其中高阶运算消去的翻译算法,翻译过程采用辅助定理证明工具Coq实现,并进行严格的正确性证明.    

3.  一个C语言安全子集的可信编译器  
   王蕾  石刚  董渊  白晓颖  王生原《计算机科学》,2013年第40卷第9期
   以安全关键领域的安全标准为依托、安全相关软件的语言编码和编译要求为指导,进行了以下几方面的研究和探索:首先对形式化验证可信编译技术进行分析研究,特别着重当前广受关注的经过验证的CompCert编译器.然后以我国安全领域C语言安全子集标准《航天型号软件C语言安全子集》为依据构造测试用例、创新测试方法,并以此对CompCert编译器进行测试评估.之后依据测试结果,为CompCert编译器增加未支持的C语言标准特性,裁剪不符合C语言安全子集要求的特性,构建符合C语言安全子集标准的可信编译器.最后的实测结果表明,所实现的编译器符合C语言安全子集标准的要求,且没有降低C代码的执行效率.    

4.  可信编译器构造的翻译确认方法简述  
   《计算机科学》,2014年第Z1期
   编译器的安全可信问题日益引起重视,特别是在安全关键系统中,编译器的误编译将会造成重大的损失。消除误编译的传统方法是大量的测试,但是测试难以达到完全覆盖,并不能充分地保证编译器的安全可信。近年来,形式化验证方法被成功用于可信编译器的构造中。一种方法是对编译器本身进行形式化验证,经过严密的证明,可杜绝误编译的发生。然而,这种方法可能"冻结"编译器的设计,阻碍编译器未来可能的优化和完善。翻译确认是另外一种用于可信编译器构造的形式化方法,它避免了对编译器自身的验证,有很好的可重用性,近年来在编译器验证领域得到了广泛研究,已取得令人瞩目的成果。介绍了翻译确认方法的概念及研究进展。    

5.  可信编译理论及其核心实现技术:研究综述  
   何炎祥  吴伟  刘陶  李清安  陈勇  胡明昊  刘健博  石谦《计算机科学与探索》,2011年第5卷第1期
   编译器是重要的系统软件之一,高级语言编写的软件都必须经过编译器的编译才能成为可执行程序。编译器的可信性对于整个计算机系统而言具有非常关键的意义,如果编译器不可信,则很难保证系统所运行软件的可信性。可信编译是指编译器在保证编译正确的同时提供相应的机制保证编译对象的可信性,对可信编译理论和技术的研究具有重要理论意义和实用前景。阐述了可信编译器的概念,介绍了编译过程正确性的形式化定义,对可信编译的主要研究进行了概括。在全面分析可信编译研究现状的基础上,从编译器自身可信性和确保编译对象可信性两个方面,对可信编译器设计和实现的相关理论和方法进行了分类和总结。最后,讨论了可信编译有待解决的问题和未来的研究方向。    

6.  出具证明编译器中代码优化与程序规范转换  
   范大威  李兆鹏  蒋信予《小型微型计算机系统》,2011年第32卷第7期
   出具证明编译器在软件安全研究得到越来越多的关注,是程序验证研究的一个重要方向.但目前关于出具证明编译器的研究主要是在程序逻辑设计和定理自动化证明方面,很少关注编译优化对规范的影响.而编译优化是决定出具证明编译器是否能走向应用的关键因素之一.通过研究数据流优化的基本行为,提出利用数据流分析结果来变换规范的方法,以使原规范的约束准确而充分地施加于优化后的代码,并实现了一个包含多种优化和相应规范转换的编译器原型系统,展示了方法的可行性.    

7.  同步数据流程序的可信排序  
   甘元科 张玲波 石 刚等《计算机应用与软件》,2014年第5期
   Lustre是一种广泛应用于核电、航空等高可信领域的同步数据流语言。用形式化验证的方法来实现Lustre到C的翻译并证明其过程能有效提高编译器的安全性。因为Lustre程序是并发执行的,需要对其进行因果分析和串行化。利用Coq工具,形式化定义拓扑排序的性质和相应层次的Lustre的语义;对Lustre程序进行因果分析和排序;证明排序后的程序满足拓扑排序的性质;证明任意两个满足拓扑排序性质的程序语义执行等价。从而实现了一种针对Lustre程序的可信排序过程。    

8.  Java虚拟机的研究与实现  
   夏兵  俞建军《计算机与信息技术》,2006年第9期
   本文在研究kaffe[1]的基础上,吸收kaffe虚拟机的主要思想,用C语言作为开发语言,采用了及时编译器作为执行引擎,实现了一种Windows平台下的Java虚拟机。然后对实现过程中的一些关键技术如class文件验证、及时编译器、垃圾收集器、线程同步和线程调度等做了分析。    

9.  编译器前端自动构造的研究与实现  
   王馨梅  王冬芳《计算机技术与发展》,2004年第14卷第4期
   编译器是高级语言的工作基础,它本身是一种复杂的程序.文中研究并实现了编译器前端的自动构造技术,能大大提高编译类软件的开发效率.重点讨论了如何合理设置接口,以便综合运用词法、语法分析器的自动构造工具LEX和YACC.提出了预置三级错误陷阱来分别俘获源程序词法、语法、语义错误的思想,能减少错误级联,并能更准确地报告错误的性质.作者已应用该技术编写出一个面向C语言的并行语言编译器前端,验证了该技术是可行的和高效的.    

10.  编译器前端自动构造的研究与实现  被引次数:1
   王馨梅 王冬芳《微机发展》,2004年第14卷第4期
   编译器是高级语言的工作基础,它本身是一种复杂的程序。文中研究并实现了编译器前端的自动构造技术,能大大提高编译类软件的开发效率。重点讨论了如何合理设置接口,以便综合运用词法、语法分析器的自动构造工具LEX和YACC。提出了预置三级错误陷阱来分别俘获源程序词法、语法、语义错误的思想,能减少错误级联,并能更准确地报告错误的性质。作者已应用该技术编写出一个面向C语言的并行语言编译器前端,验证了该技术是可行的和高效的。    

11.  出具证明编译器中线性整数命题证明的自动生成  
   杨思敏  李兆鹏  庄重  张臻婷《小型微型计算机系统》,2011年第32卷第6期
   近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.    

12.  前言  
   何炎祥  吴伟《计算机研究与发展》,2012年第49卷第9期
   随着信息技术的发展和普及,软件在计算机系统中的作用越来越重要.软件的可信性受到了日益广泛的关注.高级语言编写的软件必须经过编译才能在硬件上执行,因此编译器的可信性直接影响软件的可信性.概括地讲,可信编译是指编译器在保证编译过程正确性(编译前的源代码和编译后的目标代码语义一致)的同时,确保生成的目标代码是可信的.可信编译器不仅仅实现语义保持的代码转换功能,还    

13.  数据流分析的关键技术研究  被引次数:1
   汪小飞  赵克佳  田祖伟《计算机科学》,2005年第32卷第12期
   数据流分析在编译优化中起着非常关键的作用,尤其是想实现一个具有技术主动权的高性能优化编译器,对数据流分析方法的研究必不可少。本文介绍了数据流分析方法的基本概念和基本原理,介绍了数据流方程的一种解决方法。并结合GCC这个具体的编译器,简要分析了其中数据流分析的具体实现方法。    

14.  面向应用的可重构编译器ASCRA(英文)  被引次数:1
   吴艳霞  顾国昌  孙延腾  杨敏  杨杰  牛晓霞  孙霖《计算机科学与探索》,2011年第5卷第3期
   在很多应用领域已经开展了可重构计算的研究,但是由于缺乏高层设计工具,设计者需要较深的软件和硬件专业知识才能开发GPP/RAU架构的程序,阻碍了其大规模应用。提出了一种面向应用的可重构编译器——ASCRA的初始架构,它可以自动将C语言映射为VHDL语言,从而解决可重构计算中自动编译工具的瓶颈。ASCRA编译器主要研究软硬件划分技术和面向硬件的优化技术,如脉动阵列、循环流水技术。在ML505开发平台上,设计实现了ASCRA编译器的验证平台,并通过实验给出了核心程序段生成VHDL代码的综合信息。    

15.  基于面向对象技术的MiniC编译器的设计与实现  
   王岚《计算机与现代化》,2014年第1期
   针对传统编译器过于抽象复杂的不足,本文提出MiniC实例语言,采用面向对象技术实现该语言的编译器。MiniC编译器可以演示复杂的程序分析过程,给出编译各阶段的详细分析结果,使编译原理中的抽象内容可视化。实际应用表明,MiniC编译器在促进人们对编译理论的理解和提高系统软件开发能力方面能够发挥重要作用。    

16.  一种面向对象编译器体系结构框架  被引次数:5
   林奕  朱怡安  付游《西北工业大学学报》,2002年第20卷第3期
   对编译系统体系结构进行了新的研究和探索,基于传统编译理论和新的发展趋势,提出了基于领域模型的面向对象编译系统构造框架OOCF,以及编译过程对象化与基于程序设计语言基本规律的设计思想,并实现了一个分析系统的原型,取得了较好效果。    

17.  计算机综合实验C语言编译器设计探讨——基于LLVM架构的MIPS后端移植分析  
   王力生  王 田《计算机教育》,2014年第1期
   针对如今计算机专业实验教学过程中存在的验证性实验为主,实验内容以单点技术为主,效果比较差等问题,提出一种以MIPS I指令集子集处理器为目标机的C语言编译器的实现方案,作为实验改革方案的编译原理实验部分。该方案基于LLVM开源项目,与传统的编译原理实验方案相比,使用现代化的编译器构造工具,其内容更加新颖,实用性更强。    

18.  编译系统中间代码的一种抽象表示  
   戴桂兰  张素琴  田金兰  蒋维杜《电子学报》,2002年第30卷第Z1期
    中间表示是提高编译器的可移植性和代码生成的有效性的关键技术.为提高编译成份的可复用性,简化编译器的构造,本文提出了一种描述程序语言抽象语法及编译器内部数据结构的抽象中间表示AIR(Abstract Inter-mediate Representation).AIR以代数数据类型为主体,并用面向对象特征对其进行扩展,从而使之具有简洁的语法,较强的表达能力、灵活性和可扩展性.AIR将抽象描述与其具体实现相分离,可方便地用不同的高级程序语言实现,从而有助于提高编译成份间的互操作性.    

19.  基于XML Schema技术的编译符号表生成方法  被引次数:1
   聂南  谢晓东  甘勇《计算机科学》,2007年第34卷第5期
   传统的编译中间代码通常不能在移动、嵌入式和分布式等环境之间转换,而符号表的构造与管理贯穿整个中间代码的生成过程。本文提出一种基于XML Schema及其相关技术生成编译中间代码的符号表的方法。首先给出整体方案,然后阐述了如何运用XML Schema等技术表示编译器的前端,以及后端的目标机体系结构。生成的编译器符号表能通过XML工具统一管理和验证,从而使生成的编译中间代码有较高的可移植性,能被不同环境中的编译器采用。    

20.  SIMD计算机的优化编译器设计  
   赵辉  黄石《计算机工程》,2009年第35卷第1期
   利用处理器的相关资源,提高编译器优化性能和增强代码可适应性是SIMD处理器优化编译的关键。该文基于M语言和LSSIMD体系结构,结合现代编译器的编译技术,提出针对SIMD协处理器编译器的优化和实现方法,包括寄存器分配、单值合并、代码压缩等。实验结果表明,编译生成的目标代码准确、高效。    

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号