Concolic Unbounded-Thread Reachability via Loop Summaries (Extended Technical Report)

TL;DR

This paper introduces a novel concolic approach that combines symbolic loop summaries with explicit-state backward search to efficiently verify safety properties in multi-threaded programs with unbounded threads.

Contribution

It presents a static analysis technique to collapse loops into Presburger constraints, enabling more efficient safety verification of unbounded-thread systems.

Findings

Effective loop summarization accelerates backward search.

Method successfully proves and refutes safety properties.

Demonstrated power on multi-threaded program verification.

Abstract

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.