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

摘要：

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

关键词：程序验证、并行程序分析、可达状态空间约简

所属期刊栏目：5

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金61073052,61173021

在线出版日期：2015-05-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：18-20