Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement

TL;DR

The paper addresses the time cost of automatic software verification by parallelizing trace abstraction refinement to leverage multi-core CPUs. It introduces a coordinator–worker architecture that analyzes multiple syntactic traces in parallel, performing feasibility checks and interpolant automaton generation concurrently while a central coordinator updates the global trace abstraction. The key contributions are the conceptual parallelization of trace abstraction via diverse trace selection, an interpolant-based refinement mechanism, and the integration of this approach into Ultimate Automizer, plus a large-scale evaluation on SVBenchmark tasks showing improved effectiveness and substantial response-time reductions with more workers. The results demonstrate that parallel trace abstraction can significantly speed up verification on time-consuming tasks and complement existing parallelization techniques, enabling more practical use in continuous integration and large-scale verification pipelines.

Abstract

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.

Figures (5)

• Figure 1: Source code (left) and program automaton (right) of our example NotZero
• Figure 2: An interpolant automaton for trace $!(x>0),!(x>-10),!(x!=0)$
• Figure 3: Scatter plot that compares the wall time of PAR-2-UA (left), PAR-4-UA (middle), and PAR-6-UA (right) with the wall time of PAR-1-UA (y-axes) on tasks solved by both configurations. Additionally, points outside the rectangle represent tasks either not solved by PAR-1-UA (top) or PAR-2-UA, PAR-4-UA, and PAR-6-UA (right)
• Figure 4: Speed up on tasks for which PAR-1-UA responds more slowly. Grouped by the wall time of PAR-1-UA into the intervals $[0,10)$, $[10, 100)$, and $[100,\infty)$. On the left, we only consider tasks with property violations (alarms) while on the right we only consider tasks that adhere to the specification (proofs).
• Figure 5: Comparing the wall time of our approach PAR-6-UA (x-axis) and competitor DSS (y-axis)