A Verification Method Of Multi-threaded Program Based On SMT And BP

Multi-threaded programs are the core of computer software design.How to effectively verify the safety of multi-threaded programs has become the main research content of researchers all over the world.Existing research shows that many safety problems over finite-data replicated multi-threaded programs are decidable via a reduction to the coverability problem in certain types of well-ordered transition systems.Owing to the importance of this problem,much efforts have since been invested into finding practically viable algorithms.The vast majority of these are flavors of explicit-state exploration methods.Since the state space of multi-threaded programs grows exponentially with the increase of the size of the program and the number of threads,these algorithms have the problem of inefficiency or incompleteness.How to avoid state space search or reduce the size of state space in the verification process is the key to improve the security verification of multi-threaded programs.In this article,we consider the automated verification of such Boolean programs where an infinite number of threads execute a given finite-data procedure in parallel.Such Boolean programs are typically obtained as predicate abstractions of multi-threaded programs.According to the advantages and disadvantages of the current multi-threaded program verification method,it is considered that the symbol analysis method based on SMT solver can avoid the search of state space to speed up the verification,and directly using Boolean program as an abstract model can reduce the size of state space.A new multi-threaded program security verification method proposed in this paper.Firstly,we studies the symbol analysis module based on SMT solver,and analyzes in detail how to use the counter abstraction to construct the thread state equation of the coverability problem from the thread transition system.After the thread state equation is processed by the SMT solver,the safety of the multi-threaded program can be judged according to the output of the solver;Unsafe programs cannot be verified because the thread state equation over-approximate the coverability problem,so an efficient and complete KM algorithm based on Boolean program proposed in this paper.Second,we further studied the relationship between Boolean program and thread transition system.By analyzing the transition rules between the global state in the thread transition system and the program state in the Boolean program,the KM algorithm acting on the state transition system is directly applied to the Boolean program,and we analyze the maximum coverability succession calculation method of KM algorithm.Due to the forward search,the coverability problem is related to the initial number of threads.In order to reduce the extra memory usage in the search process,we improve KM algorithm by processing the thread state equation with the SMT solver to output a solution model that is coverability.The number of initial threads output by the SMT solver is used as the initial number of threads of the KM algorithm.If the search process is not satisfied,a complete KM algorithm is performed to obtain an efficient unsafe program verification module.Finally,we the design and implementation of the SMT-based symbol analysis module and the Boolean program-based explicit-state search module are proposed.The experimental results show that the proposed method not only accelerates the time of multi-threaded program verification,but also reduces the memory usage during the verification process.