spinnews.gif (1514 bytes)

NewsLetter 33 - September 14, 2001:

The Spin 2002 Workshop

The Spin 2002 workshop will be held April 11-13 2002 in Grenoble, France, as a satellite event of ETAPS 2002, which is held from April 6-14 2002 at the same location.

The invited speakers for our workshop are: Ed Clarke (CMU, USA), together with Allen Emerson and concurrently with Joseph Sifakis in France, one of the founders of logic model checking, and Patrick Cousot (ENS, Paris), famous for his pioneering work in abstract interpretation.

Note the submission deadline for the workshop: December 12, 2001. The call for papers is available at: http://tele.informatik.uni-freiburg.de/spin2002/

The Spin Workshops have obtained the sponsorship of ACM SIGSOFT, and the workshop now has a general chair (Moshe Vardi), a charter, a steering committee and an advisory committee. For more details, e.g. the initial membership of the two committees, see the charter description at http://tele.informatik.uni-freiburg.de/spin-charter.html.

Ruys' Recipes Available

Theo Ruys, now assistant professor at the University of Twente, has kindly made the text of his complete PhD Thesis available online, both as pdf and postscript, see Theo's homepage at http://www.cs.utwente.nl/~ruys/ (Theo's Spin Recipes can be found in Chapters 1-4.) For more details contact Theo Ruys at [email protected]

Related tools: HF-Spin

HF-SPIN is an experimental extension of Spin that uses heuristic search techniques for finding errors faster. The most practical use of this tool is that it can use an error trail file to reproduce the error state and use this information to perform a search for finding a shorter trail. At the moment HSF-SPIN allows this only for safety errors, but we are working on the extension for liveness. A first distribution of this tool is available at: http://www.informatik.uni-freiburg.de/~lafuente/hsf-spin For mode details contact Alberto Lafuente at [email protected]

Commercial Spin Licenses

Spin is distributed freely in source form to encourage research in formal verification, and the free exchange of code and ideas in this area. The software has so far been distributed under Bell Labs copyright only for research and educational use, without any guarantees whatsoever of course. For this general use no license is required. For commercial use of Spin, we have now obtained permission to issue a basic license, that is available to anyone free of charge. For details, see the Spin Public license page at http://cm.bell-labs.com/cm/cs/what/spin/spin_license.html.

The current version of Spin is 3.4.8. Sources are available through netlib as always. Precompiled executables are online for Windows, SGI, and Linux machines, at:


End of Newsletter Nr. 33.

Spin Homepage ,