一种用于指针程序验证的指针逻辑

• 作者: 华保健 李兆鹏 王志芳 陈意云
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 软件安全 Hoare逻辑 指针逻辑 携带证明的代码 出具证明的编译器
• 年，卷（期）: 2010,（3）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 415-426
• 页数: 12页
• 分类号: TP301
• 字数: 11148字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2010.03620

摘要

本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈意云	中国科学技术大学计算机科学与技术学院	83	854	16.0	26.0
3	华保健	中国科学技术大学计算机科学与技术学院	17	116	6.0	10.0
4	王志芳	中国科学技术大学计算机科学与技术学院	5	75	5.0	5.0
8	李兆鹏	中国科学技术大学计算机科学与技术学院	17	99	7.0	9.0