基于约束依赖图的并发程序模型检测工具

苏杰杨祖超田聪段振华

摘要：

模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技术缩小并发程序探索空间.针对粗糙的独立性分析会显著增加需探索的等价类路径问题,开发了一款可细化线程迁移依赖性分析的并发程序模型检测工具CDG4CPV.首先,构造了待验证可达性性质对应的规约自动机;随后,根据线程迁移边的类型和共享变量访问信息构建约束依赖图;最后,利用约束依赖图剪裁控制流图在展开过程中的独立可执行分支.在SV-COMP 2022竞赛的并发程序数据集上进行了对比实验,并对…展开v

关键词：约束依赖图、偏序约简、并发程序、模型检测、工具

所属期刊栏目：34

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

资助基金：国家自然科学基金;国家自然科学基金;国家自然科学基金;国家自然科学基金;科技创新新一代人工智能重大项目

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

页数：共16页

页码：3064-3079