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

Parallel Verification Strategy Based on Dependence Analysis

作　　者：陶荣[1] 何锫[1,2] 黄道昌[1] 

机构地区：[1]长沙理工大学计算机与通信工程学院,长沙410076 [2]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《计算机工程》2010年第12期64-65,68,共3页Computer Engineering

基　　金：武汉大学软件工程国家重点实验室基金资助项目(SKLSE20080701)

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

关 键 词：HOARE逻辑 依赖分析 并行验证 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]