with Spin

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

      discover       learn       use       community

Open Source: Starting with Version 6.4.5 from January 2016, all Spin sources and executables are available under a standard BSD 3-Clause open source license.

Workshop: The 23rd Spin 2016 Symposium will be co-located with ETAPS-2016 and held 7-8 April 2016 in Eindhoven, The Netherlands. The organizers are Dragan Bošnački and Anton Wijs, both from Eindhoven University. As always, the proceedings will be published by Springer in its LNCS series.
    • Papers are due: 18 January 2016 new
    • Author notifications: 12 February 2016
    • Camera ready papers: 24 February 2016

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.

Tau Tool: New simple front-end tool for Spin, called Tau ('Tiny Automata'): http://authors.library.caltech.edu/56038/.
It is distributed under LPL (a version of GPL) by Caltech, as a teaching tool for formal verification and finite state 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);
    	flag[_pid] = 1;
    	turn = _pid;
    	(flag[1 - _pid] == 0 || turn == 1 - _pid);
    	assert(ncrit == 1);	// critical section
    	flag[_pid] = 0;
    	goto again
    // analysis: 
    // $ spin -a peterson.pml
    // $ cc -o pan pan.c
    // $ ./pan

[revert to the old spin homepage]