CEGAR Based Array Bound Checking In C Programs

With the rapid development of computer hardware, the size of software becomes larger and larger, the complexity has been ever-increasing and the applications have become wider. Meanwhile, the number of flaws and vulnerabilities in the software systems is growing. Software security problem is more and more prominent. Therefore, how to ensure the correctness, the reliability and the safety of the software systems is one of the most significant issues in software development.As a kind of important automatic verification technique, model checking has become an important approach to enhance reliability and security of software systems. C language is one of the most widely used programming languages in software development. Since the syntax of C is very flexible, defects could be easily left if not enough attentions are paid on. Array bound is a common kind of fault in programs written in C. How to check array bound in C programs is an important and meaningful work. This thesis proposes a CEGAR based array bound verification approach in C programs. First, CEGAR based PPTL model checking of C programs is studied. Second, formal description of array bound is discussed. Finally, array bound is verified by checking whether the program satisfies the property. In order to verify array bound fully automatically, a technique for generating PPTL formulas that express array bound in C programs is investigated and implemented. Also, in order to improve the efficiency of the verification, loops in C programs are classified into different groups and dealt with separately.