Spin is a widely used open-source software verification tool.
The tool can be used for the
formal verification of multi-threaded software applications.
The tool was developed at
Bell Labs in the Unix group of the Computing
Sciences Research Center, starting in 1980, and
has been available freely since 1991. Spin
continues to evolve to keep pace with new developments in the field.
In April 2002 the tool was awarded the ACM
System Software Award.
Open Source: Starting with Version 6.4.5 from January 2016,
the Spin sources are available under the standard BSD 3-Clause open source license.
Spin is now also part of the latest stable release of Debian Linux, and
has made it into the 16.10+ distributions of Ubuntu.
The current Spin version is 6.4.9 (December 2018).
Symposia: The 27th International Spin Symposium
will be co-located with ISSTA 2021, and held 14-15 July, 2021 in Aarhus, Denmark.
organized by Alfons Laarman and Ana Sokolova.
Preprints from the proceedings of previous workshops and symposia,
are available, see symposia.
- Papers are due: March 1, 2021
- Author notifications: May 14, 2021
- Camera ready papers: June 1, 2021
Course: An online course
in software verification and logic model checking is available (password required).
There are a total 15 short lectures covering the automata-theoretic verification
method, the basic use of Spin, model extraction from
C source code, abstraction methods, and swarm verification techniques.
You can see an overview via this link.
An excellent introduction to the basics of model checking.
Interactive Static Analysis:
Take a look at:
where you can find information on a somewhat
different approach to static source code analysis.
The Cobra tool is fast enough to be used interactively
on quite large code bases. Executables to evaluate
the tool are available for Linux, Cygwin/Windows, and Mac.
Tau Tool: A simple front-end tool for Spin, called Tau
(short for Tiny Automata) can be downloaded from:
and is distributed under
by Caltech, as a teaching tool for formal verification and finite automata.
// a small example spin model
// Peterson's solution to the mutual exclusion problem (1981)
bool turn, flag; // the shared variables, booleans
byte ncrit; // nr of procs in critical section
active  proctype user() // two processes
assert(_pid == 0 || _pid == 1);
flag[_pid] = 1;
turn = _pid;
(flag[1 - _pid] == 0 || turn == 1 - _pid);
assert(ncrit == 1); // critical section
flag[_pid] = 0;
// $ spin -run peterson.pml