===================================
SPIN NEWS - Nr. 1 - January 3, 1995
===================================

There are close to 1,100 sites where the SPIN
verification software is now installed.  This
is a nice enough number to start supporting
SPIN users a little more actively.  This
first issue of the SPIN News mailing goes only to
a select number of people (approx 140) that have
in the last few months asked about the verifier
and its applications, and a few honorary recipients.
The next issue will only go to those who ack this
mail (see pt 1. below).

The main reason for these mailings is to have a channel
to send out brief reminders whenever an update of the
SPIN software takes place - bug fixes, extensions, or
major improvements such as the switch to Version 2.0.

Two other types of items can also be included in
such mailings: (a) answers to frequently asked
questions from SPIN users about modeling, complexity
control, algorithms etc., and (b) announcements or
question from people who would like to get in touch
with other SPIN users.

The new SPIN Version 2.0, available from January 1 1995 on,
includes a significantly richer specification language,
as well as an implementation of a partial order reduction
technique that preserves all safety and liveness properties,
and that is compatible with all existing verification modes
supported by SPIN.  With the reduction, problem sizes of yet
another order of magnitude larger may have come within reach
of formal verification techniques.

	Retrieval:
	SPIN Version 2.0 can be retrieved in source form
	- together with some documentation and with a
	graphical interface called xspin - freely via
	anonymous ftp from the machine netlib.att.com
	in directory /netlib/spin
	to unpack and install:
		uncompress spin2_0.tar.Z
		tar -xf spin2_0.tar
		cd Src; make
	or follow the guidelines in README.spin2

Attached below is a quick summary of the main projects
that are being pursued with SPIN, as far as I am aware
of them at least.  Since several projects are pursued
in parallel in different places, it may be useful to
distribute this type of information on a more regular
basis to the SPIN mailing list.

1. If you would like to be on the list to receive these
   mailings, please send a one line message by return
   mail, saying just: `subscribe to SPIN list'

2. If you would like to add something to the project list
   below (or modify an existing entry) - let me know.

3. If you have a question or announcement that could be
   of especial value to other SPIN users (e.g. papers
   you've written, or extensions you've made, or would
   like other to make) - send the information to me and
   i'll collect such things for this mailing list.

4. If you'd like to volunteer to moderate this mailing list,
   let me know!

5. Feel free to forward this mail to others whom you think
   might be interested in this list or the SPIN software.


Appendix:

==========================================================
Some of the projects to apply or extend the SPIN software.
==========================================================

1  Real-Time Extensions based on the Alur-Dill algorithm
   contact: Costas Courcoubetis, Stavros Tripakis
	courcou@ics.forth.gr
	tripaki@ics.forth.gr

2  Other extensions for specifying real-time properties:
   contact: Tadanori Mizuno
	mizuno@cs.shizuoka.ac.jp

3  Extensions for statistical simulations
   contact: Roberto Manione
	manione@cselt.stet.it

4  Extensions for hardware generation; hardware/software codesign
   contact: Geoffrey Brown
	gbrown@ee.cornell.edu

5  Extensions for modeling remote procedure calls and multi-threaded
   processes in distributed computing environments such as DCE and ANSA.
   contact: Joe Lin
	fjlin@bellcore.com

6  Extensions and applications of SPIN to feature-interaction problems
   in telecommunication software.
   contact: Joe Lin
	fjlin@bellcore.com

7  Extensions for sleep-set based partial order reduction
   contact: Pierre Wolper, Patrice Godefroid
	pw@montefiore.ulg.ac.be
	god@research.att.com

8  Extensions of Xspin to allow breakpointing
   contact: Thierry Cattel
	cattel@ltidec1.epfl.ch

9  Modelling and verification of the Harmony multiprocessor
   real-time kernel
   contact: Thierry Cattel
	cattel@ltidec1.epfl.ch

10 Translators from Lotos to Promela
   contact: Nicholaos Petalidis
	npetalid@cee.hw.ac.uk
   contact: Stephane Baier
	baier@res.enst.fr

11 A port of Spin version 1.6 to the Macintosh
   contact: Bob Johnston
	70302.1761@compuserve.com

12 Translator from SDL to Promela
   contact: Graham Wheeler
	gram@aztec.co.za

13 Extension for reduction using compositional approach
   and context constraints
   contact: Shing-chi Cheung
	scc@cs.ust.hk

14 Verification of railway signaling: train data bus, relay circuits,
   client-server protocols.
   contact: Peter van Eijk
	pve@cvi.ns.nl

last updated: Jan. 4, 1995