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

来源：计算机研究与发展杂志2016年第1期北京时间：

作者：段钊,田聪,段振华,

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

关键词：模型检测, 抽象精化, 空指针解引用, 程序验证, 时序逻辑,