Guides students through algebraic specification and verification of distributed systems, and some of the formal verification techniques. This book employs [mu]CRL as the vehicle, a language developed to combine process algebra and abstract data types.