Research And Implementation Of C Program Loop Verification Method Based On Model Checking

With the rapid progress of computer technology,it is hard for people to do work without the computer.A wide range of software appears one after another,and the scale of the software are increasing day by day,which makes testing unable to satisfy the requirements for detecting the software vulnerabilities.In order to reduce the software vulnerabilities and ensure the accuracy and reliability of the software,many researches on the software model checking method based on source code are studied and have a great success.The counter-example guided abstraction refinement algorithm is widely used in recent years.It computes predicate by Craig interpolation,and abstracts the program with predicate.The algorithm not only alleviates the problem of state space explosion,but also maintains the accuracy of the detection results.However,for the detection of loops,it still produces too many states,which result in low detection efficiency.In order to alleviate this problem,an improved algorithm is presented in this thesis.The algorithm is based on the counter-example guided abstraction refinement algorithm,and combines the method of static analysis with dynamic execution to verify the C language program.This algorithm can help the detection of program loops and improve the detection efficiency.The loops can be divided into two types in this algorithm.One is the simple loop and the other one is the complex loop.For the simple loop,we use the method of static analysis.The number of loop unrolling is decreased by using the improved model of simple loop instead of the old one in the process of building the model,which will save a lot of space and time spent on unrolling the loop.For the complex loop,we adopt the method of dynamic execution.It extracts the information of the program when it reaches the critical point of entering a complex loop,and combines the loop body with its context into an executable code,then we compile and execute the code.The valid information after execution will be abstracted into a state of the model,then the state will be involved in the subsequent detection progress.We implement the algorithm,and make a lot of experiements,which states that our algorithm has a good effect on program verification.