反例引导的C代码空间流模型检测方法

Software verification has always been a hot research topic to ensure the correctness and security of software. However, due to the complex semantics and syntax of programming language, applying formal methods to verify the correctness of programs has the problems of low accuracy and low efficiency. Among them, the state change of address space caused by pointer operations makes the verification accuracy of existing model checking methods difficult to be guaranteed. By combining model checking and sparse value-flow analysis, this study designs a spatial flow model to effectively describe the state behavior of C codes at the symbolic variable level and address space level, and proposes a model checking algorithm of counterexample-guided abstraction refinement and sparse value flow strong update (CEGAS), which enables points-to-sensitive formal verification for C codes. This study establishes a C code benchmark containing a variety of pointer operations and conducts comparative experiments based on this benchmark. These experiments indicate that in the task of analyzing multi-class C code features, the model checking algorithm CEGAS proposed in this study can achieve outstanding results compared with the existing model detection tools. The verification accuracy of CEGAS is 92.9%, and the average verification time of each line of code is 2.58 ms, which are both better than existing testing tools.