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

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

作者机构：中国科学技术大学计算机科学与技术学院安徽合肥230026 中国科学技术大学苏州研究院软件安全实验室江苏苏州215123 中国科学技术大学软件学院安徽合肥230026 

基　　金：国家自然科学基金Nos.90718026 60928004~~ 

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2010年第21卷第2期

页      码：334-343页

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

主 题 词：软件安全 Hoare逻辑:指针逻辑 

学科分类：08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.3724/sp.j.1001.2010.03783

馆 藏 号：203541788...