ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2016, Vol. 53 ›› Issue (1): 155-164.doi: 10.7544/issn1000-1239.2016.20150669

Special Issue: 2016优青专题

Previous Articles     Next Articles

CEGAR Based Null-Pointer Dereference Checking in C Programs

Duan Zhao, Tian Cong, Duan Zhenhua   

  1. (Institute of Computing Theory and Technology, Xidian University, Xi’an 710071)
  • Online:2016-01-01

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

CLC Number: