Automatic compositional reasoning for multi-thread programs

Automatic verification for multi-threaded programs has been an important and hard branch in model checking. The multi-thread programs are infinite systems which increase the state space with the number of the threads. To alleviate the state explosion, many techniques are proposed such as abstraction and compositional reasoning. However, the environment problem is the main barrier for the compositional reasoning. As a promising approach, thread modular consider the environment of the threads through shared variables, which is incomplete for the verification. In this paper, we will extend the thread modular reasoning to achieve complete compositional reasoning for multi-thread programs. We provide the automatic refinement strategy for the environment, which is generated by exposing necessary local information. And, we will combine the invariant deductive rule, reachability analysis and thread modular model reasoning for the verification of the multi-thread programs.