The Concurrency Workbench of the New Century (CWB-NC) provides users with a number of different techniques for specifying and verifying finite-state concurrent systems. The tool combines support for several different system-design notations with decision procedures for a number of refinement relations and for determining if systems satisfy temporal formulas. The design of the tool facilitates cu