  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.
