面向程序验证的并行程序状态空间态约简技术综述

• 作者: 苏小红 赵玲玲 逄龙 马培军
• 来源期刊: 智能计算机与应用
• 学科: 工学
• 关键词: 程序验证 并行程序分析 可达状态空间约简
• 年，卷（期）: 2015,（1）
• 页码范围: 18-20
• 页数: 3页
• 分类号: TP311.5
• 字数: 3926字
• 语种: 中文

摘要

程序验证是保证程序安全性的重要手段.随着采用多核技术的硬件环境日渐普及,越来越多的软件正通过转向基于共享内存的并行程序模型来充分利用现有的计算资源.各线程在并行执行时通过共享内存的访问互相干扰执行状态,导致可能执行路径数成几何级数增长,进而产生可达状态空间爆炸问题.由于验证并行程序安全性主要通过分析程序可达状态来实现,因此,对并行程序可达状态空间的约简是决定并行程序验证效率的关键因素.首先对面向并行程序验证的并行程序可达状态空间约简方法进行了分类,然后对各类可达状态空间约简方法分别进行了分析和总结,最后指出了当前存在的问题和未来解决这些问题的研究方向.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	苏小红	哈尔滨工业大学计算机科学与技术学院	152	1551	20.0	34.0
2	马培军	哈尔滨工业大学计算机科学与技术学院	93	639	14.0	20.0
3	赵玲玲	哈尔滨工业大学计算机科学与技术学院	33	424	9.0	20.0
4	逄龙	哈尔滨工业大学计算机科学与技术学院	3	5	2.0	2.0