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 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.bell-labs.com in directory /netlib/spin to unpack and install:
```
	uncompress spin2*Src.tar.Z
	tar -xf spin2*Src.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.

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'
If you would like to add something to the project list below (or modify an existing entry) - let me know.
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.
If you'd like to volunteer to moderate this mailing list, let me know!
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.

Real-Time Extensions based on the Alur-Dill algorithm

   contact: Costas Courcoubetis, Stavros Tripakis
	courcou@ics.forth.gr
	tripaki@ics.forth.gr

Other extensions for specifying real-time properties:

   contact: Tadanori Mizuno
	mizuno@cs.shizuoka.ac.jp

Extensions for statistical simulations

   contact: Roberto Manione
	manione@cselt.stet.it

Extensions for hardware generation; hardware/software codesign
```
   contact: Geoffrey Brown
	gbrown@ee.cornell.edu
```
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
```
Extensions and applications of SPIN to feature-interaction problems in telecommunication software.
```
   contact: Joe Lin
	fjlin@bellcore.com
```

Extensions for sleep-set based partial order reduction

   contact: Pierre Wolper, Patrice Godefroid
	pw@montefiore.ulg.ac.be
	god@research.att.com

Extensions of Xspin to allow breakpointing

   contact: Thierry Cattel
	cattel@ltidec1.epfl.ch

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

Translators from Lotos to Promela

   contact: Nicholaos Petalidis
	npetalid@cee.hw.ac.uk
   contact: Stephane Baier
	baier@res.enst.fr

A port of Spin version 1.6 to the Macintosh

   contact: Bob Johnston
	70302.1761@compuserve.com

Translator from SDL to Promela

   contact: Graham Wheeler
	gram@aztec.co.za

Extension for reduction using compositional approach and context constraints
```
   contact: Shing-chi Cheung
	scc@cs.ust.hk
```
Verification of railway signaling: train data bus, relay circuits, client-server protocols.
```
   contact: Peter van Eijk
	pve@cvi.ns.nl
```

Gerard J. Holzmann (gerard@research.bell-labs.com)