Spin - Formal Verification
[banner] 


Verifying
Multi-threaded
Software
with Spin


[logo]
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. [read more]

      discover       learn       use       community
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.5.1 (July 2020).
Symposia: The 31st International Symposium on Model Checking Software will be held May 7-8 2025 in Hamilton, Canada, co-located with ETAPS-2025. The Symposium is organized by Kristin Yvonne Rozier and Gidon Ernst.
Courses: A short 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.

In-Depth: A full one semester college-level course is also available, complete with transcripts of every lecture, quizzes, assignments, and exercises to test your understanding and practice new skills. Details can be found in this syllabus.

Interactive Static Analysis: Take a look at: https://spinroot.com/cobra 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 very large code bases. A book documenting all usage options is in the works. Email if you'd like to be an early reviewer.
Tau Tool: A simple front-end tool for Spin, called Tau (short for Tiny Automata) can be downloaded from: https://spinroot.com/spin/tau_v1.tar.gz, and is distributed under LGPL, originally 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[2];		// the shared variables, booleans
    byte ncrit;        		// nr of procs in critical section
    
    active [2] proctype user()	// two processes
    {
    	assert(_pid == 0 || _pid == 1);
    again:
    	flag[_pid] = 1;
    	turn = _pid;
    	(flag[1 - _pid] == 0 || turn == 1 - _pid);
    
    	ncrit++;
    	assert(ncrit == 1);	// critical section
    	ncrit--;
    
    	flag[_pid] = 0;
    	goto again
    }
    // analysis: 
    // $ spin -run peterson.pml

[revert to the old spin homepage]