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

作     者：段钊 田聪 段振华 Duan Zhao;Tian Cong;Duan Zhenhua

作者机构：西安电子科技大学计算机理论与技术研究所西安710071 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2016年第53卷第1期

页      面：155-164页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金项目(61322202 61420106004 91418201 61133001 61272117)~~ 

主　　题：模型检测 抽象精化 空指针解引用’ 程序验证 时序逻辑 

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