Advanced Search
    Duan Zhao, Tian Cong, Duan Zhenhua. CEGAR Based Null-Pointer Dereference Checking in C Programs[J]. Journal of Computer Research and Development, 2016, 53(1): 155-164. DOI: 10.7544/issn1000-1239.2016.20150669
    Citation: Duan Zhao, Tian Cong, Duan Zhenhua. CEGAR Based Null-Pointer Dereference Checking in C Programs[J]. Journal of Computer Research and Development, 2016, 53(1): 155-164. DOI: 10.7544/issn1000-1239.2016.20150669

    CEGAR Based Null-Pointer Dereference Checking in C Programs

    • 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.
    • loading

    Catalog

      Turn off MathJax
      Article Contents

      /

      DownLoad:  Full-Size Img  PowerPoint
      Return
      Return