

The following book describes the algorithms for onthefly 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
AddisonWesley, ISBN 0321228626, 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 0135399254.
A paperback edition of the book is still available from
www.amazon.com.
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. 279295.
(PDF)

The automatatheoretic foundation for Spin:
An automatatheoretic approach to automatic
program verification,
by Moshe Y. Vardi, and Pierre Wolper,
Proc. First IEEE Symp. on Logic in Computer Science,
1986, pp. 322331.
(PDF)

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
(PDF)

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.
(PDF)

The nested depth first search algorithm used in Spin:
On nested depthfirst search,
by G.J. Holzmann, D. Peled, and M. Yannakakis,
in The Spin Verification System, pp. 2332,
American Mathematical Society, 1996. (Proc. of the 2nd Spin Workshop.)
(PDF)

Wolper's hashcompact 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. 5970.
(PDF)

The algorithm for conversion of LTL to Buchi Automata
(in Spin terminology: never claims) is described in:
Simple onthefly automatic verification of linear temporal logic,
by Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper,
Proc. PSTV 1995 Conference, Warsaw, Poland.
(PDF)
For a broader overview of conversion algorithms, see:
http://spot.lip6.fr/wiki/LtlTranslationAlgorithms

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.
(PDF)

The method for the use of embedded C code in Spin verification models
(introduced in Spin Version 4):
Logic Verification of ANSIC Code with Spin,
by G.J. Holzmann,
Proc. SPIN2000, Springer Verlag, LNCS 1885, pp. 131147.
(PDF)
and the abstraction method it supports is described in
ModelDriven Software Verification,
by G.J. Holzmann and R. Joshi,
Proc. SPIN2004, Springer Verlag, LNCS 2989, pp. 7792.
(PDF)

The algorithms for the extension to multicore model checking
(introduced in Spin Version 5) are described in:
The Design of a multicore extension of the Spin Model Checker ,
by G.J. Holzmann and D. Bosnacki,
IEEE Trans. on Software Engineering, Vol. 33, No. 10, pp. 659674.
(PDF)

The algorithms that are used to support swarm verification (supported through the
swarm preprocessor to Spin,
and Spin Version 5.2) are described in:
Swarm Verification,
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.
(PDF)
(an expanded journal version appears in:
IEEE Trans. on Software Engineering, Vol. 37, No. 6, Nov/Dec 2011, pp. 845857)

The design and implementation in Spin version 5.2.5 of a
new and powerful bounded context switching algorithm is detailed in:
Model checking with bounded context switching,
by G.J. Holzmann and M. Florian,
Formal Aspects of Computing Vol. 23, No. 3 (May 2011), pp. 365389,
DOI=10.1007/s0016501001605.
(PDF)
Spin home page
 