收缩候选回溯集的有状态动态偏序归约方法

摘要：

在验证多线程并发程序时，将基于无状态或有状态搜索的软件模型检测与动态偏序归约方法相结合，能大幅缩减待验证程序的状态空间，而动态偏序归约需不断利用当前候选回溯集更新相应回溯集，导致更新回溯集的计算成本过高。为此，形式化定义收缩候选回溯集，消除原候选回溯集中满足同一回溯条件的冗余迁移。针对各交织的回溯点，使用当前收缩候选回溯集更新相应回溯集，实现基于有状态动态偏序归约方法的并发多线程程序验证。实验结果表明，与现有动态偏序归约方法相比，该方法能减少遍历迁移数，加速回溯集更新，提高动态软件模型检测效率。

关键词：软件模型检测、动态偏序归约、有状态搜索、回溯集、收缩候选集

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

资助基金：国家自然科学基金资助项目61370083,61073043,61073041;教育部高等学校博士学科点专项科研基金资助项目20112304110011,20122304110012;哈尔滨市科技创新人才研究专项基金资助项目2011RFXXG015。

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

页数：共7页

页码：70-76