An efficient formal verification method for concurrent programs

Formal methods (FM) are a pivotal technology for ensuring the safety and reliability of software systems. These methods are centered around the application of precise mathematical principles to verify the security and dependability of software. Formal methods have been widely employed in the verification of critical systems, with the increasing significance of concurrent programs in the context of the growing prevalence of parallel computing architectures like multi-core processors. However, the efficiency of formal methods in verifying concurrent programs is often low, which hinders their broader adoption and application. Addressing this issue, this study proposes an efficient formal verification method tailored for concurrent programs. This method bifurcates the verification process of concurrent programs into two stages: proving sequential correctness and verifying other attributes. In the first stage, leveraging theorem-proving strategies and large language model (LLM) technology, the method assists in proving the sequential correctness of concurrent programs. The second stage, based on model checking technology, involves transforming the program to narrow down the verification scope before using model checking tools to verify other security attributes of the program. Experimental results have shown that the proposed method significantly reduces the state space that needs to be searched during verification, thereby enhancing the efficiency of concurrent program verification.