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 ruys@cs.utwente.nl.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 lafuente@informatik.uni-freiburg.de.
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
,
spin_list@research.bell-labs.com
ftp://cm.bell-labs.com/cm/cs/what/spin/Bin/spin348.exe
ftp://cm.bell-labs.com/cm/cs/what/spin/Bin/spin348_sgi
ftp://cm.bell-labs.com/cm/cs/what/spin/Bin/spin348_linux