基于CEGAR的C程序空指针解引用检测

• 作者: 段振华 段钊 田聪
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 模型检测 抽象精化 空指针解引用 程序验证 时序逻辑
• 年，卷（期）: 2016,（1）
• 所属期刊栏目: 优青专题
• 页码范围: 155-164
• 页数: 10页
• 分类号: TP31
• 字数: 6929字
• 语种: 中文
• DOI: 10.7544/issn1000-1239.2016.20150669

摘要

随着计算机软件规模和复杂度的日益增长,软件系统的可靠性和安全性倍受关注.空指针解引用是程序中常见的一类错误.提出了一种基于反例制导抽象精化CEGAR的C程序空指针解引用检测方法.该方法首先使用线性时序逻辑描述空指针解引用问题,然后通过抽象精化的方法检测待测程序中是否含有空指针解引用错误.为了达到完全自动验证的目标,同时针对空指针解引用问题,研究了该类性质的时序逻辑表达方法,并自动从程序中针对所有的指针变量,形成相应的时序逻辑公式.实验结果表明,所提出的方法在大规模C程序的空指针解引用检测方面有着重要的实际应用价值.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	段振华	西安电子科技大学计算机理论与技术研究所	47	363	10.0	16.0
2	田聪	西安电子科技大学计算机理论与技术研究所	8	41	4.0	6.0
3	段钊	西安电子科技大学计算机理论与技术研究所	2	10	2.0	2.0