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

Peizun Liu, Thomas Wahl

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 n…