中文摘要：

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

英文摘要：

With the rapid growth of computer software in both scale and complexity, more and more attention has been paid by software developers on the reliability and security issue. Null-pointer dereference is a kind of errors which often occur in programs. This paper proposes a CEGAR based null-pointer dereference verification approach for C programs. With this method, first, a linear temporal logic （LTL） formula is used to specify the null-Pointer dereference problem. Then whether null-pointer dereference occuring in a program is checked by a CEGAR based model checking approach. In order to verify null, pointer dereference problem in a total automatic way, this paper also studies how to generate temporal logic formulas automatically with respective to null-pointer dereference problem. Experimental results show that the proposed approach is useful in practice for checking null-pointer dereference in C programs with large scale.