1983 Trace. In 1983 replaced by Trace [H85]. The switch from Pan/Pandora to Trace signalled a change from a verification method based on process algebras [H82] to one that is based on automata. This was originally done for efficiency considerations only, to allow for the construction of a more effective tool. Later, an effective automata based verification theory was developed that justified the switch better still, [VW86].

1987 SuperTrace. In 1987 Trace was replaced with an experimental tool called Supertrace [H88], and in 1988 this experimental tool was integrated into SdlValid [H89] (a verifier for CCITT (now ITU) standard SDL specifications).

1989 Spin. The first version of Spin was written in 1989 to serve as a small example model checking system that could be discussed in a course on protocol verification [H91]. The on-the-fly verification paradigm is now extended in its application to the verification of omega-regular properties in general (including, but not restricted to, linear temporal logic), [H97].

1994 Partial Order Reduction. After many experiments with various reduction methods, Spin was extended in 1994 with a static reduction technique (named STREM, for Static Reduction Method) based on a general theory for partial order reduction [HP94].

1995 LTL conversion. A year later Spin was extended with a builtin algorithm for converting from LTL syntax to automata. The method is based on the algorithm described in [GPVW95].

1997 Minimized Automata. Another significant extension of Spin was the addition of an algorithm for representing the reachable state space with a BDD-like representation that is optimized for application to software verification problems. In software, for instance, one rarely sees as many boolean variables as in hardware. Data is more naturally captured in byte or word-size quantities. Like the partial order reduction technique, the minimized automaton representations can, in some cases, reduce memory requirements exponentially. There is, however, a time penalty for the use of the more compact state representations. The algorithm and its implementation are described in [HP99].

1999 Statement Merging. In version 3.3 of Spin we added a statement merging technique that is more fully explained in [H99]. The technique, though a fairly straightforward extension of partial order reduction rules, can significantly reduce memory use and runtime for the model checker.

2000 Property-based Slicing. The most recent addition to Spin is a property-based slicing technique that can prove beneficial in combination with automated model extraction. More details on this algorithm appear in the lecture notes to the 2000 Summerschool at Marktoberdorf, published by Springer Verlag [H00b].

2003 Support for embedded C code. Spin Version 4.0 contains direct support for embedded C code fragments, which offers the required infrastructure for model checking of ANSI-C programs, through the use of a model extractor [H00a, H03, HJ04].
Also new in Version 4.0.1 is support for breadth-first search [H03].

2007 Support for multicore systems. Spin Version 5.0 contains support for model checking on multicore systems, as detailed in [HB07].

2008 Support for swarm verification. Spin Version 5.1.5 contains support for swarm verification techniques, which can make optimal use of large numbers of available compute cores to leverage parallelism and search diversification techniques, which increases the chance of locating defects in very large verification models (see swarm) [HJG08a,HJG08b,HJG10].

2010 Support for Bounded Context Switching. Spin Version 5.2.5 contains support for bounded context switching, which can home in on counter-examples with small numbers of unforced context switches between active processes [HF10].
Spin version 6.0 added support for multiple never claims and inline LTL formulae.

2012 Support for Parallel BFS and Priority-based scheduling. Spin Version 6.2.0 contains support for parallelizing the breadth-first search on multicore machines -- with support for the verification of both safety and liveness properties. Also added is a new verification mode to support verification of embedded software, which is often based on priority based scheduling rules. [H12].

2016 Spin Version 6.4.5 released under BSD 3-Clause license. The first version of Spin that was released under a standard open source BSD license, replacing the earlier somewhat non-standard Lucent open software release.

• [GPVW95] R. Gerth, D. Peled, M. Vardi, P. Wolper, Simple on-the-fly automatic verification of linear temporal logic, Proc. PSTV 1995 Conference, Warsaw, Poland. (PDF)
• [H81] G. J. Holzmann, PAN - a protocol specification analyzer, Bell Laboratories Technical Memorandum, TM81-11271-5, May 1981. (PDF)
• [H82] --, A Theory for Protocol Validation, IEEE Trans. on Computers, Aug. 1982, Vol C-31, No 8, pp. 730-738.7-391 (PDF)
• [H83] --, and R. A. Beukers, The PANDORA protocol development system, Proc. 3rd Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP, Eds. H. Rudin and C. West, pp. 357--369, North Holland Publ. Co., June, 1983. (PDF)
• [H85] --, Tracing protocols, AT&T Techn. Journal, Vol 64, No. 10, Dec. 1985. (PDF)
• [H87] --, Automated protocol validation in Argos, assertion proving, scatter searching, IEEE Trans. on Software Eng., Vol SE-13, No 6, June 1987, pp. 683-696. (PDF)
• [H88] --, An improved reachability analysis technique, Software Practice and Experience, Vol. 18, No. 2, pp. 137-161, Feb. 1988. (PDF)
• [H89] --, and J. Patti, Validating SDL specifications: an experiment, Proc. 9th Int. Conf on Protocol Specification, Testing, and Verification, INWG/IFIP, Ed. C. Vissers and E. Brinksma, Twente, Netherlands, June, 1989. (PDF)
• [H91] --, Design and Validation of Computer Protocols, Prentice Hall, 1991. (PDF)
• [HP94] --, and D. Peled, An improvement in formal verification, Proc. Forte94, Berne, Switzerland, 1994. (PDF)
• [H97] G.J. Holzmann, The model checker Spin, IEEE T/SE, Vol. 23, No. 5, May 97, pp. 279-295. (PDF)
• [VW86] Moshe Y. Vardi, and Pierre Wolper, An automata-theoretic approach to automatic program verification, Proc. First IEEE Symp. on Logic in Computer Science, 1986, pp. 322-331.
• [HP99] G.J. Holzmann, and A. Puri, A Minimized Automaton Representation of Reachable States, Software Tools for Technology Transfer, Vol. 2, No. 3, November 1999, Springer Verlag, pp. 270-278. (PDF)
• [H99] G.J. Holzmann, The engineering of a model checker: the Gnu i-protocol case study revisited, Proc. of the 6th Spin Workshop, Toulouse, France, September 1999. (LNCS 1680, Springer Verlag). (PDF)
• [H00a] G.J. Holzmann, Logic Verification of ANSI-C Code with Spin, Proc. SPIN2000, Springer Verlag, LNCS 1885, pp. 131-147. (PDF)
• [H00b] G.J. Holzmann, Software Model Checking, Course notes, NATO Summer School, Marktoberdorf, Germany, Aug. 2000, IOS Press, Computer and System Sciences, Vol. 180, pp. 309-355. (PDF)
• [H03] G.J. Holzmann, The Spin Model Checker: Primer and Reference Manual, Addison-Wesley, Sept. 2003, 608 pgs.
• [HJ04] G.J. Holzmann and R. Joshi, Model-Driven Software Verification, Proc. 11th Spin Workshop, Barcelona, Spain, April 2004, Springer Verlag, LNCS 2989, pp. 77-92. (PDF)
• [HB07] G.J. Holzmann and D. Bosnacki, The design of a multi-core extension of the Spin model checker, IEEE Trans. on Software Engineering, Vol. 33, No. 10, pp. 659-674. (PDF)
• [HJG08a] G.J. Holzmann, R. Joshi, A. Groce, Tackling large verification problems with the Swarm tool
  15th Spin Workshop, UCLA, Los Angeles, August 2008, LNCS 5156. (PDF)
• [HJG08b] G.J. Holzmann, R. Joshi, A. Groce, Swarm Verification, Proc. ASE 2008, 23rd IEEE/ACM Int. Conf. on Automated Software Engineering, l'Aquila, Italy, Sept. 2008. (PDF)
• [HJG10] G.J. Holzmann, R. Joshi, A. Groce, Swarm Verification Techniques, IEEE Trans. on Software Engineering, 2010 (to appear).
• [HF10] G. J. Holzmann, M. Florian, Model checking with bounded context switching, Formal Aspects of Computing, 2010.
• [H12] G. J. Holzmann, Parallelizing the Spin Model Checker, Proc. 19th Spin Workshop, Oxford, England, 23-24 July 2012, LNCS, Springer Verlag.