The following book describes the algorithms for on-the-fly verification,
the underlying theory, the specification language and the tool options,
for the current version of Spin.
The Spin Model Checker: Primer and Reference Manual
Addison-Wesley, ISBN 0-321-22862-6, 608 pgs, 2004.
The book contains a complete set of manual pages for every language
construct in Promela, and explain Spin's simulation and verification options.
An earlier book (Nov. 1990) describing Spin was:
Design and Validation of Computer Protocols,
Prentice Hall, New Jersey, 1991, ISBN 0-13-539925-4.
A paperback edition of the book is still available from
There is also a Japanese translation of the book.
An overview paper of Spin, with verification examples, is:
The Model Checker Spin,
IEEE Trans. on Software Engineering,
Vol. 23, No. 5, May 1997, pp. 279-295.
The automata-theoretic foundation for Spin:
An automata-theoretic approach to automatic
by Moshe Y. Vardi, and Pierre Wolper,
Proc. First IEEE Symp. on Logic in Computer Science,
1986, pp. 322-331.
The algorithm for bitstate hashing (optional in Spin for verifying
large problem sizes) is discussed in detail in:
An analysis of bitstate hashing,
by G.J. Holzmann, Formal Methods in Systems Design, Nov. 1998
The algorithm for partial order reduction is described in:
An Improvement in Formal Verification,
by G.J. Holzmann and D. Peled,
Proc. FORTE 1994 Conference, Bern, Switzerland.
The nested depth first search algorithm used in Spin:
On nested depth-first search,
by G.J. Holzmann, D. Peled, and M. Yannakakis,
in The Spin Verification System, pp. 23-32,
American Mathematical Society, 1996. (Proc. of the 2nd Spin Workshop.)
Wolper's hash-compact method (optional in Spin version 3.2.1 and later)
was first presented and analyzed in:
Reliable hashing without collision detection,
by Pierre Wolper and Dennis Leroy,
Proc. 5th Int. Conference on Computer Aided Verification, 1993,
Elounda, Greece, pp. 59-70.
The algorithm for conversion of LTL to Buchi Automata
(in Spin terminology: never claims) is described in:
Simple on-the-fly automatic verification of linear temporal logic,
by Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper,
Proc. PSTV 1995 Conference, Warsaw, Poland.
For a broader overview of conversion algorithms, see:
The algorithm for storing reachable states with a minimized automaton
(introduced in Spin Version 3):
A Minimized automaton representation of reachable states,
by A. Puri and G.J. Holzmann,
Software Tools for Technology Transfer, Vol. 3, No. 1, Springer Verlag.
The method for the use of embedded C code in Spin verification models
(introduced in Spin Version 4):
Logic Verification of ANSI-C Code with Spin,
by G.J. Holzmann,
Proc. SPIN2000, Springer Verlag, LNCS 1885, pp. 131-147.
and the abstraction method it supports is described in
Model-Driven Software Verification,
by G.J. Holzmann and R. Joshi,
Proc. SPIN2004, Springer Verlag, LNCS 2989, pp. 77-92.
The algorithms for the extension to multi-core model checking
(introduced in Spin Version 5) are described in:
The Design of a multi-core extension of the Spin Model Checker ,
by G.J. Holzmann and D. Bosnacki,
IEEE Trans. on Software Engineering, Vol. 33, No. 10, pp. 659-674.
The algorithms that are used to support swarm verification (supported through the
swarm preprocessor to Spin,
and Spin Version 5.2) are described in:
by G.J. Holzmann, R. Joshi, A. Groce,
Proc. ASE 2008, 23rd IEEE/ACM Int. Conf. on Automated Software Engineering,
l'Aquila, Italy, Sept. 2008.
(an expanded journal version will appear in the IEEE Trans. on Software Engineering.)
To appear: a journal paper on the implementation in Spin version 5.2.5 of a
new and powerful bounded context switching algorithm.
Spin home page