DIMACS: Series in Discrete Mathematics and Theoretical Computer Science 1997; 203 pp; hardcover Volume: 32 ISBN10: 0821806807 ISBN13: 9780821806807 List Price: US$60 Member Price: US$48 Order Code: DIMACS/32
 What is Spin? Spin is a general tool for the specification and formal verification of software for distributed systems. It has been used to detect design errors in a wide range of applications, such as abstract distributed algorithms, data communications protocols, operating systems code, and telephone switching code. The verifier can check for basic correctness properties, such as absence of deadlock and race conditions, logical completeness, or unwarranted assumptions about the relative speeds of correctness properties expressed in the syntax of Lineartime Temporal Logic (LTL). The tool translates LTL formulae automatically into automata representations, which can be used in an efficient onthefly verifications procedure. This DIMACS volume presents the papers contributed to the second international workshop that was held on the Spin verification system at Rutgers University in August 1996. The work covers theoretical and foundational studies of formal verification, empirical studies of the effectiveness of different types of algorithms, significant practical applications of the Spin verifier, and discussions of extensions and revisions of the basic code. Copublished with the Center for Discrete Mathematics and Theoretical Computer Science beginning with Volume 8. Volumes 17 were copublished with the Association for Computer Machinery (ACM). Readership Graduate students, theorists and practicioners in formal methods, formal verification of software and automata theory. Table of Contents  J.C. Grégoire  State space compression with graph encoded sets
 G. J. Holzmann and O. Kupferman  Not checking for closure under stuttering
 G. J. Holzmann, D. Peled, and M. Yannakakis  On nested depth first search
 H. E. Jensen, K. G. Larsen, and A. Skou  Modelling and analysis of a collision avoidance protocol using Spin and Uppaal
 P. Kars  The application of Promela and Spin in the BOS project
 S. Leue and P. B. Ladkin  Implementing and verifying MSC specifications using Promela/XSpin
 S. Löffler and A. Serhrouchni  Creating implementations from Promela models
 P. Merino and J.M. Troya  Modelling and verification of the MCS layer with Spin
 E. Najm and F. Olsen  Protocol verification with reactive Promela/Rspin
 V. Natarajan and G. J. Holzmann  Outline for an operational semantics of Promela
 S. K. Shukla, D. J. Rosenkrantz, and S. S. Ravi  A simulation and validation tool for selfstabilizing protocols
 J. Tuya, J. R. de Diego, C. de la Riva, and J. A. Corrales  Dynamic analysis of SA/RT models using Spin and modular verification
 W. Visser and H. Barringer  Memory efficient state storage in Spin
