指针逻辑

作品数：9被引量：36H指数：3
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：陈意云华保健王志芳李兆鹏葛琳更多>>
相关机构：中国科学技术大学中国科学院软件研究所更多>>
相关期刊：《计算机研究与发展》《软件学报》《小型微型计算机系统》《计算机学报》更多>>
相关基金：国家自然科学基金国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-8
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一个用于指针程序验证的自动定理证明器的设计与实现被引量：2
《小型微型计算机系统》2010年第5期801-806,共6页王振明 陈意云 王志芳 
国家自然科学基金项目(60673126;90718026)资助;Intel中国研究中心资助
对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自...
关键词：指针逻辑 验证条件 自动定理证明器 证明检查算法 
一种用于指针程序验证的指针逻辑被引量：6
《软件学报》2010年第3期415-426,共12页陈意云 李兆鹏 王志芳 华保健 
国家自然科学基金Nos.90718026;60928004~~
本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便...
关键词：软件安全 HOARE逻辑 指针逻辑 携带证明的代码 出具证明的编译器 
处理指针相等关系不确定的指针逻辑
《软件学报》2010年第2期334-343,共10页梁红瑾 张昱 陈意云 李兆鹏 华保健 
国家自然科学基金Nos.90718026;60928004~~
为类C小语言PointerC设计的指针逻辑是Hoare逻辑的一种扩展,可用来对指针程序进行精确的指针分析,以支持指针相等关系确定的程序的安全性验证.通过增加相等关系不确定的指针类型访问路径集合,可扩展这种指针逻辑,使得扩展后的指针逻辑...
关键词：软件安全 Hoare逻辑:指针逻辑 
用于指针逻辑的自动定理证明器(英文)被引量：1
《软件学报》2009年第8期2037-2050,共14页王振明 陈意云 王志芳 
Supported by the National Natural Science Foundation of China under Grant Nos.60673126,90718026~~
提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL的工具中得以实现.APL自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自...
关键词：指针程序 指针逻辑 验证条件 自动定理证明器 证明检查器 
一种汇编语言指针逻辑的设计与实现
《小型微型计算机系统》2009年第6期1025-1030,共6页李兆鹏 陈意云 华保健 王伟 田波 
国家自然科学基金项目(60673126)资助;Intel中国研究中心资助
软件的安全性日益重要,软件满足安全策略的证明方法成为一个研究热点.而指针程序的安全性质证明是难点之一.根据已经提出的安全程序设计与证明的框架以及PointerC指针逻辑,提出一种汇编语言指针逻辑.该逻辑解决了Hoare逻辑处理别名问题...
关键词：软件安全 指针逻辑 HOARE逻辑 携带证明的汇编程序 
一种汇编程序的形式验证框架被引量：3
《计算机研究与发展》2008年第5期825-833,共9页李兆鹏 陈意云 葛琳 华保健 
国家自然科学基金项目(60473068,60673126);Intel中国研究中心资助项目~~
在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关...
关键词：软件安全 出具证明编译器 指针逻辑 HOARE逻辑 携带证明的汇编程序 
安全语言PointerC的设计及形式证明被引量：8
《计算机学报》2008年第4期556-564,共9页华保健 陈意云 李兆鹏 王志芳 葛琳 江苏苏州215123 
国家自然科学基金(60673126);Intel中国研究中心资助~~
程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(sid...
关键词：软件安全 语言设计 类型系统 HOARE逻辑 指针逻辑 
一种用于指针程序安全性证明的指针逻辑被引量：21
《计算机学报》2008年第3期372-380,共9页陈意云 华保健 葛琳 王志芳 
国家自然科学基金(60673126)资助
在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,...
关键词：软件安全 指针逻辑 HOARE逻辑 指针分析 类型系统 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部