HOARE逻辑

作品数：32被引量：69H指数：4
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：陈意云李兆鹏华保健葛琳王志芳更多>>
相关机构：中国科学技术大学武汉大学解放军信息工程大学清华大学更多>>
相关期刊：《计算机工程与设计》《计算机与数字工程》《计算机与现代化》《通讯和计算机（中英文版）》更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点实验室开放基金教育部“新世纪优秀人才支持计划”更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于Hoare逻辑的密码软件安全性形式化验证方法
《吉林大学学报（工学版）》2019年第4期1301-1306,共6页肖堃 
国家科技重大专项项目(2014ZX03002001)
为了解决密码软件安全性验证效率和准确率低的问题,提出了基于Hoare逻辑的密码软件安全性形式化验证方法。首先对密码软件的主要性质进行描述,然后通过密码软件运行时随机向量的分析,得到密码软件运行的矩阵表达式,再将其进行线性变换,...
关键词：计算机系统结构 霍尔逻辑 密码软件 安全性验证 
一种基于栈区内存模型的C程序别名判断算法被引量：1
《小型微型计算机系统》2019年第2期353-358,共6页常欢 罗奇鸣 李薛剑 陈意云 
国家自然科学基金项目(61170018;61229201)资助
C语言中的指针导致C程序中会出现表达式别名的情况.在基于演绎推理的程序验证中,使用Hoare逻辑的赋值规则前必须消除断言中的别名.别名增加了程序验证的难度.本文根据C语言的语义提出了一种栈区内存模型,可以精确地跟踪栈区的多种类型...
关键词：程序验证 HOARE逻辑 内存模型 别名 栈区 
关于断言语言中引入逻辑变量的研究被引量：2
《小型微型计算机系统》2017年第5期925-929,共5页李为胜 罗奇鸣 陈意云 
国家自然科学基金项目(61170018;61229201)资助
基于Hoare逻辑推理规则去验证程序安全性的研究是程序验证领域的重要发展方向.但是在Hoare逻辑中,仅依靠程序变量的断言语言无法表达程序上下文中不变性质.本文研究通过在断言语言中引入逻辑变量的方式来表达程序上下文不变性质,同时详...
关键词：HOARE逻辑 形式化验证 逻辑变量 断言语言 
栈指针程序的形式验证被引量：2
《小型微型计算机系统》2017年第5期936-940,共5页冯峰 罗奇鸣 陈意云 
国家自然科学基金项目(61170018;61229201)资助
提出一种验证含栈指针、静态区指针操作的C语言程序的方法.该方法定义指针的三元属性表示一个指针的状态.指针的三元属性包括指针指向数据块的名称、数据块的长度以及指针在所指向数据块上的偏移.通过对Hoare逻辑的扩展,基于指针的三元...
关键词：程序验证 栈指针 静态区指针 路径别名 HOARE逻辑 
概率拟Hoare逻辑
《计算机科学》2016年第4期177-181,191,共6页吴新星 胡国胜 陈仪香 
基于Hoare逻辑,给出了概率拟Hoare逻辑,用于刻画程序执行的正确度,定量地描述理论与程序(或软件)实际执行之间的差距,反映理论被程序实现的程度,从而量化理论上正确的程序在实际执行时出错的可能性,以及解释正确度很高的两个程序串行复...
关键词：HOARE逻辑 Hoare三元组 正确度 概率测度 
[α_1,α_2]1-概率拟Hoare逻辑及其可靠性证明
《计算机科学》2015年第B11期93-99,共7页吴新星 胡国胜 陈仪香 
基于C.A.R.Hoare提出的Hoare逻辑,给出了[α_1,α_2]1-概率拟Hoare逻辑,并证明了其可靠性。
关键词：HOARE逻辑 Hoare三元组 正确度 概率测度 
断言语言支持自定义谓词的程序验证器原型被引量：3
《小型微型计算机系统》2013年第7期1482-1486,共5页徐文义 陈意云 李兆鹏 
国家自然科学基金项目(61003043;61170018)资助
基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较多限制,导致程序的某些递归性质难以用断言语言表述.本文在一个面向指针程序、基于先前自行设计的形状图...
关键词：程序验证 HOARE逻辑 形状图逻辑 程序分析 自定义谓词 
一个程序验证器的设计和实现被引量：11
《计算机研究与发展》2013年第5期1044-1054,共11页张志天 李兆鹏 陈意云 刘刚 
国家自然科学基金项目(61170018;61003043)
形式验证是提高软件可信程度的重要方法,基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点,但尚无可供工业界使用的产品,其根源在于自动定理证明方面的困难.介绍在通过程序分析建立起各程序点的形状图的基础上,如何利用形状...
关键词：程序验证 HOARE逻辑 形状图逻辑 程序分析 分离逻辑 
基于分离逻辑的程序分析技术
《火力与指挥控制》2012年第6期63-67,共5页裴芳 刘云龙 张洁 郝丽波 
湖南省教育厅科学研究基金资助项目(10C0152)
分离逻辑是John C Reynolds和Peter O'Hearn于2000年提出的基于Hoare逻辑分析程序中动态分配内存和指针别名的逻辑理论。首先回顾了分离逻辑系统的理论框架,然后讨论了分离逻辑在程序分析领域中符号执行、形态分析和并发程序分析验证这...
关键词：分离逻辑 程序分析 HOARE逻辑 形态分析 
一种用于指针程序的形状分析方法被引量：1
《计算机与现代化》2012年第4期82-85,共4页刘刚 胡凯平 宋发兴 
指针程序的分析一直是研究热点。本文提出一种基于形状图逻辑的形状分析方法,其中形状分析采用形状图来表达程序中指针的指向和相等关系,并用形状图逻辑来进行推理。形状图逻辑是一种把形状图看成有关指针的断言,并在此基础上对Hoare逻...
关键词：形状图 形状图逻辑 HOARE逻辑 形状分析 程序分析 
全选清除导出
共4页<1234>
检索报告 对象比较 聚类工具 使用帮助 返回顶部