V8.0 版权所有© 2001-2026 渝B2-20050021-1
渝公网安备 50019002500403号违法和不良信息举报中心举报邮箱：jubao@cqvip.com
互联网出版许可证 新出网证(渝)字10号机构客服热线 023-67882612
- 安全语言PointerC的设计及形式证明 认领 引用 被引量：8
- 1
- 《计算机学报》 EI CAS 北大核心 2008年第4期556-564,共9页
- 程序设计语言本身的安全性在高安全需求软件的设计和实现中起着基础作用.该文在用于系统级编程的安全语言的设计和性质证明方面,做了有益的尝试.作者设计了一个类C的命令式语言PointerC,其主要特点在于其类型系统中包含显式的副条件(sid... 展开更多
- 关键词 软件安全 语言设计 类型系统 Hoare逻辑 指针逻辑
- 一种用于指针程序安全性证明的指针逻辑 认领 引用 被引量：21
- 2
- 《计算机学报》 EI CAS 北大核心 2008年第3期372-380,共9页
- 在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,... 展开更多
- 关键词 软件安全 指针逻辑 Hoare逻辑 指针分析 类型系统
- 一种用于指针程序验证的指针逻辑 认领 引用 被引量：6
- 3
- 《软件学报》 EI 北大核心 2010年第3期415-426,共12页
- 本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便... 展开更多
- 关键词 软件安全 Hoare逻辑 指针逻辑 携带证明的代码 出具证明的编译器
- 一种汇编程序的形式验证框架 认领 引用 被引量：3
- 4
- 《计算机研究与发展》 EI 北大核心 2008年第5期825-833,共9页
- 在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关... 展开更多
- 关键词 软件安全 出具证明编译器 指针逻辑 Hoare逻辑 携带证明的汇编程序
- 一种基于指针逻辑的代码安全属性分析方法 认领 引用 被引量：3
- 5
- 《计算机学报》 EI CAS 北大核心 2009年第6期1119-1125,共7页
- 在分析和总结前人工作的基础上,提出了一种改进的代码安全属性验证方法.该方法在利用传统的源代码安全属性验证工具的基础上,加入了指针逻辑,针对现有代码属性分析技术只能对C语言子集进行分析验证的不足,利用指针逻辑对源代码的分析结... 展开更多
- 关键词 操作系统安全 形式化验证 代码分析 模型检测 指针逻辑
- 二维逻辑PPTLSL的可满足性检查 认领 引用 被引量：2
- 6
- 《软件学报》 EI CSCD 北大核心 2016年第3期670-681,共12页
- 由于指针的灵活性以及别名现象的存在,程序的运行可能会出现悬空指针引用、内存泄漏等诸多问题.PPTLSL是一种二维(时间和空间)时序逻辑,它结合了分离逻辑(separation logic)与命题投影时序逻辑PPTL(propositional projection tempora... 展开更多
- 关键词 时序逻辑 分离逻辑 指针 二维逻辑 可满足性
- 基于CEGAR的C程序空指针解引用检测 认领 引用 被引量：2
- 7
- 《计算机研究与发展》 EI CSCD 北大核心 2016年第1期155-164,共10页
- 随着计算机软件规模和复杂度的日益增长,软件系统的可靠性和安全性倍受关注.空指针解引用是程序中常见的一类错误.提出了一种基于反例制导抽象精化CEGAR的C程序空指针解引用检测方法.该方法首先使用线性时序逻辑描述空指针解引用问题,... 展开更多
- 关键词 模型检测 抽象精化 空指针解引用’ 程序验证 时序逻辑
- 一种汇编语言指针逻辑的设计与实现 认领 引用
- 8
- 《小型微型计算机系统》 北大核心 2009年第6期1025-1030,共6页
- 软件的安全性日益重要,软件满足安全策略的证明方法成为一个研究热点.而指针程序的安全性质证明是难点之一.根据已经提出的安全程序设计与证明的框架以及PointerC指针逻辑,提出一种汇编语言指针逻辑.该逻辑解决了Hoare逻辑处理别名问题... 展开更多
- 关键词 软件安全 指针逻辑 Hoare逻辑 携带证明的汇编程序
- 用于指针逻辑的自动定理证明器(英文) 认领 引用 被引量：2
- 9
- 《软件学报》 EI 北大核心 2009年第8期2037-2050,共14页
- 提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL的工具中得以实现.APL自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自... 展开更多
- 关键词 指针程序 指针逻辑 验证条件 自动定理证明器 证明检查器
- 一个用于指针程序验证的自动定理证明器的设计与实现 认领 引用 被引量：2
- 10
- 《小型微型计算机系统》 北大核心 2010年第5期801-806,共6页
- 对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自... 展开更多
- 关键词 指针逻辑 验证条件 自动定理证明器 证明检查算法
- 栈指针程序的形式验证 认领 引用 被引量：2
- 11
- 《小型微型计算机系统》 CSCD 北大核心 2017年第5期936-940,共5页
- 提出一种验证含栈指针、静态区指针操作的C语言程序的方法.该方法定义指针的三元属性表示一个指针的状态.指针的三元属性包括指针指向数据块的名称、数据块的长度以及指针在所指向数据块上的偏移.通过对Hoare逻辑的扩展,基于指针的三元... 展开更多
- 关键词 程序验证 栈指针 静态区指针 路径别名 Hoare逻辑
- 一个统一的异构对象持久化框架 认领 引用 被引量：1
- 12
- 《计算机工程》 EI CAS 北大核心 2004年第18期78-80,共3页
- 以大型对象系统PG-RELIEF为对象,考察一般大型对象系统在持久化管理上的需求,然后提出基于面向对象范型的统一对象持久化框架并对之进行分析。
- 关键词 持久化对象 持久化系统 面向对象设计 逻辑指针 应用系统构造
- 多维数组与其指针之间的逻辑对应关系研究 认领 引用
- 13
- 《辽宁师专学报（自然科学版）》 2015年第2期45-47,共3页
- 为灵活应用多维数组指针,研究了多维数组指针与多维数组之间的逻辑关系.通过分析多维数组的构造方法及多维数组指针常量和多维数组指针变量的内涵,指出多维数组指针与多维数组之间的逻辑对应关系.
- 关键词 多维数组 多维数组指针 逻辑关系
- 基于实例的C程序指针调试介绍 认领 引用
- 14
- 《黑龙江科技信息》 2008年第4期61-61,共1页
- 基于实例介绍Turbo C 2.0环境下的调试工具的应用。在分析实例的过程中指出了调试程序能够帮助学生理解书本上的知识,还给出了一个检查逻辑错误的例子。
- 关键词 调试 逻辑错误 指针
- C语言中常见错误分析 认领 引用 被引量：2
- 15
- 《电脑知识与技术（过刊）》 2009年第9X期7447-7449,共3页
- C语言是许多高校开设的第一门程序设计语言,使用方便灵活。根据C语言的特点,并结合实际教学,对在编程中经常遇到的错误进行分析、总结,为初学者尽快掌握C语言,提高程序设计水平提供借鉴。
- 关键词 C语言 常见错误 逻辑错误 指针 变量
