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

摘要：

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

关键词： 软件安全 指针逻辑 类C小语言 访问路径集合 有向图 抽象数据结构

作者: 梁红瑾 张昱 陈意云 李兆鹏 华保健

作者单位: 中国科学技术大学少年班学院，安徽 合肥 230026 中国科学技术大学计算机科学与技术学院，安徽 合肥 230026 中国科学技术大学软件学院，安徽 合肥 230026

会议类型: 国内会议

会议名称: 中国计算机学会全国软件与应用学术会议(NASAC2009)

会议地点: 沈阳

会议语种:中文

页码: 7-14

在线出版日期: 2009-09-22（万方平台首次上网日期，不代表论文的发表时间）