处理指针相等关系不确定的指针逻辑

• 作者: 华保健 张昱 李兆鹏 梁红瑾 陈意云
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 软件安全 Hoare逻辑 指针逻辑
• 年，卷（期）: 2010,（2）
• 页码范围: 334-343
• 页数: 10页
• 分类号: TP311
• 字数: 9340字
• 语种: 中文

摘要

为类C小语言PointerC设计的指针逻辑是Hoare逻辑的一种扩展,可用来对指针程序进行精确的指针分析,以支持指针相等关系确定的程序的安全性验证.通过增加相等关系不确定的指针类型访问路径集合,可扩展这种指针逻辑,使得扩展后的指针逻辑可以应用于有向图等指针相等关系不确定的抽象数据结构上的指针程序性质证明.