Dynamic Execution Based Complex Loop Verification Of C Program

The rapid development of computer technology plays an important role in the development of various fields. However, it also brings lots of unexpected damages because of defects in software systems. Software testing can be used to exclude some of the defects, but there are still a large number of software defects which cannot be detected by software testing.Model checking is an important way to ensure the quality of software systems. Compared with software testing, model checking is good at finding the deeply hidden defects. In the most popular programming languages, C has been widely used by industry. However, problems like memory-leak, array-bound, and visiting invalid memory chunks, etc. often occur in C programs due to its flexible syntax, permission to access memory directly, and not checking the bound of arrays. To check these problems, it is hard to avoid the state space explosion problem. Even in abstraction-refinement based approach, it often runs out of memory especially for loops with complex statements inside. To solve this problem, in this thesis, we propose a new method called dynamic execution based complex loop verification of C programs. First, we find complex loops in a program according to the rules and mark them in the syntax tree. Then, we extract the context information about loop from SMT solver and construct an executable program with respect to the complex loop. Finally, we record the results after executing the complex loop and provide them to the rest of the program to be the initialization. As a result, we improve the efficiency in processing complex loop compared with the static method.