Concolic Unbounded-Thread Reachability via Loop Summaries (Extended Technical Report)
This work addresses the challenge of scalable verification for concurrent systems, which is crucial for ensuring reliability in multi-threaded software, though it appears incremental as it builds on existing backward search methods.
The paper tackles the problem of verifying safety properties in systems with arbitrarily many finite-state threads by accelerating explicit-state backward search algorithms, achieving significant speedups through loop summarization without approximation.
We present a method for accelerating explicit-state backward search algorithms for systems of arbitrarily many finite-state threads. Our method statically analyzes the program executed by the threads for the existence of simple loops. We show how such loops can be collapsed without approximation into Presburger arithmetic constraints that symbolically summarize the effect of executing the backward search algorithm along the loop in the multi-threaded program. As a result, the subsequent explicit-state search does not need to explore the summarized part of the state space. The combination of concrete and symbolic exploration gives our algorithm a concolic flavor. We demonstrate the power of this method for proving and refuting safety properties of unbounded-thread programs.