Multi-Threaded Software Model Checking via Parallel Trace Abstraction Refinement

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 its 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 may violate the safety property in parallel. We realize our parallelized version of trace abstraction in the verification tool ULTIMATE AUTOMIZER and perform a thorough evaluation. Our evaluation shows that our parallelization is more effective than sequential trace abstraction and provides 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.