An efficient algorithm to compute the synchronized product

Computing all the reachable states of synchronized automata is important in the mechanical verification of concurrent programs. It is however a hard task because this set of states typically grows exponentially in the number of automata involved. We present a new approach that yields interesting experimental results, both an memory requirements and computation times. It uses a new data structure, the sharing tree, which allows to store large sets of states in a compact way. Moreover, we have designed algorithms that use global operations and caching on the data structure itself