A tool, called PAX has been implemented based on the work in [BLS01]. The tool has been used to verify several parametrized protocols, e.g. Szymanski's mutual exclusion algorithm
The paper [CAS01] describes the tool TREX which implements symbolic reachability analysis techniques for different classes of infinite-state systems. The tool is used for automatic synthesis of invariants in a parametrized version of the IEEE 1394 root contention protocol.