The Concurrency Workbench: A Semantics Based Tool for the Verification
of Concurrent Systems

R. Cleaveland, J. Parrow, B. Steffen

	   The Concurrency Workbench is an automated tool for analyzing
	   networks of finite-state processes expressed in Milner's
	   Calculus of Communi- cating Systems. Its key feature is its
	   breadth: a variety of different verification methods, including
	   equivalence checking, preorder checking and model checking,
	   are supported for several different process semantics. One
	   experience from our work is that a large number of interesting
	   verification methods can be formulated as combinations of a
	   small number of primitive algorithms.  The Workbench has been
	   applied to the verification of communications protocols and
	   mutual exclusion algorithms and has proven a valuable aid in
	   teaching and research.