We consider the class of finite-state programs executed by an unbounded number of replicated threads communicating via shared variables. The
problem for this class is essential in software verification using predicate abstraction. While this problem is decidable via
Petri net coverability
analysis, techniques solely based on coverability suffer from the problem’s exponential-space complexity. In this paper, we present an alternative method based on a
: a number
of threads that suffice to generate all reachable thread states. We give a condition, verifiable dynamically during reachability analysis for increasing
, that is sufficient to conclude that
is a cutoff. We then make the method complete, via a coverability query that is of low cost in practice. We demonstrate the efficiency of the approach on Petri net encodings of communication protocols, as well as on non-recursive Boolean programs run by arbitrarily many parallel threads.