Theoretical Background

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

• The automata-theoretic foundation for Spin:

     An automata-theoretic approach to automatic
     program verification,
     by Moshe Y. Vardi, and Pierre Wolper,
     Proc. First IEEE Symp. on Logic in Computer Science,
     1986, pp. 322-331.
     (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 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.)
     (PDF)
  

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

• 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.
     (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 ANSI-C Code with Spin,
    by G.J. Holzmann,
    Proc. SPIN2000, Springer Verlag, LNCS 1885, pp. 131-147.
    (PDF)
  
  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.
    (PDF)
  

• 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.
    (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 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.