Automatic software verification is a valuable means for software quality assurance. However, automatic verification and in particular software model checking can be time-consuming, which hinders their practical applicability e.g., the use in continuous integration. One solution to address the issue is to reduce the response time of the verification procedure by leveraging today's multi-core CPUs. In this paper, we propose a solution to parallelize trace abstraction, an abstraction-based approach to software model checking. The underlying idea of our approach is to parallelize the abstraction refinement. More concretely, our approach analyzes different traces (syntactic program paths) that could violate the safety property in parallel. We realize our parallelized version of trace abstraction in the verification tool Ulti mate Automizer and perform a thorough evaluation. Our evaluation shows that our parallelization is more effective than sequential trace abstraction and can provide results significantly faster on many time-consuming tasks. Also, our approach is more effective than DSS, a recent parallel approach to abstraction-based software model checking.

翻译：自动软件验证是保障软件质量的重要手段。然而，自动验证（尤其是软件模型检测）往往耗时较长，这限制了其在实际场景中的应用，例如在持续集成中的使用。解决该问题的一种途径是通过利用当今的多核CPU来缩短验证过程的响应时间。本文提出一种并行化迹抽象的解决方案，迹抽象是一种基于抽象的软件模型检测方法。我们方法的核心思想是并行化抽象精化过程。具体而言，我们的方法并行分析可能违反安全性质的不同迹（语法程序路径）。我们在验证工具Ultimate Automizer中实现了并行化迹抽象版本，并进行了全面评估。评估结果表明，我们的并行化方法比顺序迹抽象更高效，能够在许多耗时任务上显著加快结果获取速度。此外，与近期基于抽象的软件模型检测并行方法DSS相比，我们的方法也表现出更优的性能。