出具证明编译器

作品数：8被引量：10H指数：2
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：李兆鹏陈意云葛琳华保健杨思敏更多>>
相关机构：中国科学技术大学更多>>
相关期刊：《计算机工程与应用》《小型微型计算机系统》《计算机研究与发展》《计算机工程》更多>>
相关基金：国家自然科学基金江苏省自然科学基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-8
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
支持用户自定义谓词的自动定理证明的研究
《小型微型计算机系统》2013年第8期1781-1786,共6页汪娟 李兆鹏 陈意云 
国家自然科学基金项目(61003043;61170018)资助
在先前设计的一个出具证明编译器原型基础上,增加了可用来描述数据结构性质的自定义谓词,对断言语言表达能力方面做了提升.在出具证明编译器的框架内,借助自动定理证明技术,针对自定义谓词的特点,设计了专门的推理规则,由此实现自定义...
关键词：出具证明编译器 自定义谓词 自动定理证明 推理规则 
出具证明编译器中代码优化与程序规范转换被引量：2
《小型微型计算机系统》2011年第7期1400-1405,共6页范大威 李兆鹏 蒋信予 
国家自然科学基金项目(90718026;60928004)资助
出具证明编译器在软件安全研究得到越来越多的关注,是程序验证研究的一个重要方向.但目前关于出具证明编译器的研究主要是在程序逻辑设计和定理自动化证明方面,很少关注编译优化对规范的影响.而编译优化是决定出具证明编译器是否能走向...
关键词：规范转换 代码优化 数据流分析 出具证明编译器 
一种出具证明编译器中的汇编级断言和证明生成的方法被引量：1
《小型微型计算机系统》2011年第6期1164-1169,共6页张臻婷 李兆鹏 陈意云 杨思敏 庄重 
国家自然科学基金项目(90718026)资助;江苏省自然科学基金项目(BK2008181)资助
携带证明代码允许代码消费方通过检查代码生产方提供的证明,来判断代码是否满足相应的安全规范.本文实现了一个类C语言的出具证明编译器原型,它在将带有规范标注的源代码编译成汇编代码的同时,还能产生汇编代码满足相应规范的Coq可检查...
关键词：程序验证 携带证明代码 出具证明编译器 汇编级验证 
出具证明编译器中线性整数命题证明的自动生成被引量：1
《小型微型计算机系统》2011年第6期1175-1180,共6页杨思敏 李兆鹏 庄重 张臻婷 
国家自然科学基金项目(90718026;60928004)资助
近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译...
关键词：证明生成 自动定理证明 整数定理证明 出具证明编译器 
一个出具证明编译器后端的设计与实现被引量：1
《计算机工程》2009年第7期132-135,共4页田波 陈意云 王伟 李兆鹏 王志芳 
国家自然科学基金资助项目(60673126;90718026);Intel中国研究中心基金资助项目
设计并实现一个类C语言PointerC的出具证明编译器后端。该后端采用最强后条件演算同步处理整型断言和指针断言实现整型验证条件和指针验证条件的证明,能够完全自动地产生目标级程序的指针安全性证明,处理常见递归数据结构中的非一致性...
关键词：高可信软件 出具证明编译器 指针安全 汇编代码 
汇编代码验证中的形式规范自动生成被引量：3
《小型微型计算机系统》2008年第7期1219-1224,共6页葛琳 陈意云 华保健 李兆鹏 刘诚 
国家自然科学基金项目(60673126)资助;Intel中国研究中心项目资助
与传统的高级语言程序验证相比,汇编代码验证中所需要的形式规范往往比较复杂,通常的做法是要求程序员手写形式规范,或是牺牲形式规范的表达能力以期能够自动生成规范.本文提出一种能够自动生成形式规范的方法,该方法依托一个出具证明...
关键词：出具证明编译器 汇编代码验证 形式规范Hoare逻辑 前(后)条件 
一种汇编程序的形式验证框架被引量：3
《计算机研究与发展》2008年第5期825-833,共9页李兆鹏 陈意云 葛琳 华保健 
国家自然科学基金项目(60473068,60673126);Intel中国研究中心资助项目~~
在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关...
关键词：软件安全 出具证明编译器 指针逻辑 HOARE逻辑 携带证明的汇编程序 
一个出具证明编译器原型系统的实现被引量：1
《计算机工程与应用》2007年第21期99-102,114,共5页刘诚 陈意云 葛琳 华保健 
国家自然科学基金(the National Natural Science Foundation of China under Grant No.60673126);Intel中国研究中心资助。
出具证明编译器是随着人们对现今的软件提出更高的可靠性和安全性要求而产生的工具,它结合了以往程序设计和程序安全性证明的技术。论文介绍了一个出具证明编译器原型系统的实现。
关键词：软件安全 出具证明编译器 验证条件 形式化证明方法 证明生成器 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部