CEGAR Based Null-pointer Dereference Checking In C Programs

With the rapid development of computer hardware, computer software systems are more and more complex, and the size of the systems is larger and larger. Thus, more and more errors are hidden in the code. Therefore, how to improve reliability and security of the software systems has become a very urgent demand in computer software community.Model checking is an important approach to enhance reliability and security of software systems. It can verify whether or not a software system satisfies the desired properties automatically. Among kinds programming languages, C is one of the most widely used ones in building software systems. It is well known that grammar of C is flexible. In particular, in case a pointer is not carefully used, a program crash occurs possibly because of memory leak, uninitialized pointers, many times memory release, and null pointer dereference.With this motivation, this thesis proposes a CEGAR based null pointer dereference verification approach in C programs. To do so, CEGAR based PPTL model checking of C programs is studied first. As a result, by describing the property of null-pointer dereference with PPTL formulas, we can further check whether or not there is a null pointer dereference in a C program. Meanwhile, a technique for automatically generate PPTL formulas that express null-pointer dereference in programs is also investigated in this thesis. To evaluate the implemented approach, a tool named PPTLChecker has been developed for detecting null pointer dereference in C programs automatically. The experimental results show that PPTLChecker is useful in practice in detecting null pointer dereference in C programs.