DIMACS Series in
Discrete Mathematics and Theoretical Computer Science
VOLUME Thirty Two
TITLE: "The Spin Verification System"
EDITORS: Jean-Charles Grégoire, Gerard J. Holzmann
and Doron A. Peled.
This volume may be obtained from the AMS or through bookstores in your area.
To order through AMS contact the AMS Customer Services Department, P.O. Box
6248, Providence, Rhode Island 02940-6248 USA. For Visa, Mastercard,
Discover, and American Express orders call 1-800-321-4AMS.
You may also visit the
AMS Bookstore and
order directly from there.
DIMACS does not distribute or sell these books.
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 Linear-time Temporal Logic (LTL). The tool translates
LTL formulae automatically into automata representations, which
can be used in an efficient on-the-fly verifications
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.
- J. Grégoire -- State space compression with graph encoded sets
- G. J. Holzmann and O. Kupferman -- Not checking for closure under stuttering
- J. G., 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. Troya -- Modelling and verification of the MCS layer with Spin
- E. Najm and F. Olsen -- Protocol verification with reactive Promela/Rspin
- V. Natarajan and J. G. -- Outline for an operational semantics of Promela
- S. K. Shukla, D. J. Rosenkrantz, and S. S. Ravi -- A simulation and validation tool for self-stabilizing 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
Index of Volumes
Contacting the Center
Document last modified on October 28, 1998.