Spin is a popular open-source software verification tool,
used by thousands of people worldwide. 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.
The software has been available freely since 1991, and
continues to evolve to keep pace with new developments.
In April 2002 the tool was awarded the ACM
System Software Award.
Tau Tool: New simple front-end tool for Spin, called Tau ('Tiny Automata'):
It is distributed under LPL (a version of GPL) by Caltech,
as a teaching tool for formal verification
and finite state automata.
Course: An online course
in software verification and logic model checking is now available
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.
Workshop: The Spin 2015 workshop
is held at the University of Stellenbosch, in South Africa,
24-26 August 2015.
The workshop organizers are Bernd Fischer and Jaco Geldenhuys.
The workshop proceedings will be published by Springer in its LNCS series.
- Abstracts are due: 17 April 2015
- Full papers: 24 April 2015
- Author notifications: 15 June 2015
- Camera ready papers: 6 July 2015
// 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 -a peterson.pml
// $ cc -o pan pan.c
// $ ./pan