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

Abstract: 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.

Key words: model checking, abstraction refinement, null-pointer dereference, program verification, temporal logic