基于依赖分析的并行化验证策略

提高验证过程的并行性是提高程序验证效率的重要手段之一。为此，提出一种基于控制结构依赖分析的方法来组织程序的并行验证，在验证过程中，并行验证完的控制结构直接触发支持控制结构，无须等待其他操作，从而可以提高程序验证的并行性。此外，还给出提取控制结构依赖图算法和验证过程调度算法，并用实验证明其正确性和高效性。

Parallel Verification Strategy Based on Dependence Analysis

One of the important means to increase the efficiency of program verification is to fully develop the parallelism. So a method which is based on the dependence analysis of control structures to organize it is proposed. In the process of verification, the parallel verified control structure can trigger the supported control structure, and there is no need to wait for other operations, so it can enhance the parallelism for verification of programs. Algorithms as well as experiments for extracting the dependence diagram of control structures, scheduling of verification process, and demonstrating their correctness and efficiency are also introduced.