作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2010, Vol. 36 ›› Issue (12): 64-65. doi: 10.3969/j.issn.1000-3428.2010.12.022

• 软件技术与数据库 • 上一篇    下一篇

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

陶 荣1,何 锫1,2,黄道昌1   

  1. (1. 长沙理工大学计算机与通信工程学院,长沙 410076;2. 武汉大学软件工程国家重点实验室,武汉 430072)
  • 出版日期:2010-06-20 发布日期:2010-06-20
  • 作者简介:陶 荣(1985-),男,硕士研究生,主研方向:形式化验证;何 锫,教授、博士;黄道昌,高级工程师
  • 基金资助:
    武汉大学软件工程国家重点实验室基金资助项目(SKLSE20080701)

Parallel Verification Strategy Based on Dependence Analysis

TAO Rong1, HE Pei1,2, HUANG Dao-chang1   

  1. (1. College of Computer and Communication Engineering, Changsha University of Science and Technology, Changsha 410076;2. State Key Laboratory of Software Engineering, Wuhan University, Wuhan 430072)
  • Online:2010-06-20 Published:2010-06-20

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

关键词: Hoare逻, 依赖分析, 并行验证

Abstract: 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.

Key words: Hoare logic, dependence analysis, parallel verification

中图分类号: