We consider the verification problem of programs with unbounded (1) recursive procedure calls, and (2) dynamic creation of concurrent processes. Programs are modeled using term rewrite systems called PRS (for process rewrite systems). These models are more powerful than pushdown automata and Petri nets, two common models for reasoning about, respectively, recursive programs without process creation, and multi-threaded programs without recursive calls. A PRS can actually be seen as the nesting of prefix rewrite system and a multiset rewrite system.
We define a generic procedure which constructs a finite representation of the set of all reachable configurations of a given PRS, provided that its underlying multiset rewrite system is semilinear. We represent PRS reachability sets by means of a new class of tree automata with unbounded width. Our procedure can be instantiated in different ways leading to new reachability analysis procedures for PRS.