Unbounded-Thread Reachability via Symbolic Execution and Loop Acceleration (Technical Report)

TL;DR

This paper introduces a symbolic execution and loop acceleration method to analyze parameterized reachability in concurrent programs with unbounded threads, effectively handling loops and simplifying the verification process.

Contribution

It presents a novel approach combining symbolic execution with loop acceleration into Presburger constraints for unbounded-thread reachability analysis.

Findings

Efficiently accelerates simple loops into Presburger constraints.

Exact satisfiability of constraints indicates program state reachability.

Method effectively proves safety properties in infinite-state systems.

Abstract

We present an approach to parameterized reachability for communicating finite-state threads that formulates the analysis as a satisfiability problem. In addition to the unbounded number of threads, the main challenge for SAT/SMT-based reachability methods is the existence of unbounded loops in the program executed by a thread. We show in this paper how simple loops can be accelerated without approximation into Presburger arithmetic constraints. The constraints are obtained via symbolic execution and are satisfiable exactly if the given program state is reachable. We summarize loops nested inside other loops using recurrence relations derived from the inner loop's acceleration. This summary abstracts the loop iteration parameter and may thus overapproximate. An advantage of our symbolic approach is that the process of building the Presburger formulas may instantly reveal their unsatisfiability, before any arithmetic has been performed. We demonstrate the power of this technique for proving and refuting safety properties of unbounded-thread programs and other infinite-state transition systems.