SPIN NEWS - Nr. 10 - March 19, 1996

Contents of this NewsLetter:

The SPIN96 Workshop

DIMACS Sponsorship

The Second International Spin Workshop will be sponsored by DIMACS this year -- (DIMACS is the NSF Science and Technology Center for Discrete Mathematics and Theoretical Computer Science, a consortium that includes Rutgers and Princeton University, and research labs such as Bellcore, Bell Labs, and AT&T Research). DIMACS is organizing a special year on Logic and Algorithms, and is hosting several major international conferences in New Jersey this year, such as LICS (Logic in Computer Science), and CAV (Computer Aided Verification), and a range of smaller workshops. More information on the special year can be found via URL: http://dimacs.rutgers.edu/.

Venue and Proceedings

As a result, the venue of our workshop will most likely move to Rutgers University -- in the same buildings where the other conferences and workshops will be held. It also means that the Proceedings of the SPIN96 Verification Workshop will now be officially published by the AMS (the American Mathematical Society) as a book in the DIMACS series. The Proceedings will most likely not actually appear in its final form before 1997, but it gives welcome additional exposure to the SPIN Workshop participants. Authors of the papers that are presented at the workshop will have time to submit a final edited version of the papers after the workshop itself -- details will follow when the time gets closer.

SPIN Updates since last Newsletter

The current version of Spin is Version 2.8. The main change, justifying the move up from 2.7 to 2.8, is that the current version of Spin is the first one that can be used on either generic Unix systems and on PCs. Both the Spin software itself and the Xspin Tcl/Tk interface have been adapted to work without change on either platform.
You minimally need working (and recent) versions of gcc and of Tcl/Tk. Use the newest version 7.5/4.1 -- previous Windows ports of Tcl/Tk had many internal problems that were fixed in the latest release -- currently that is the file `win41b3.exe' which can be obtained via anonymous ftp from ftp.smli.com in directory /pub/tcl
If you have Tcl/Tk and Gcc installed in the default places on your PC, you can also use the precompiled version of Spin/Xspin which is available from netlib.bell-labs.com as file: /netlib/spin/pc_spin280.zip
To compile your own version, you also need a PC version of yacc (e.g., the public domain Berkeley Yacc version called byacc), and can compile spin.exe with the following 3 commands:

	byacc -v -d spin.y
	gcc -DPC *.c -o spin
	coff2exe spin
This port of SPIN will work on any PC system. The Tcl/Tk version of XSPIN will work on WINDOWS95 systems, but (because of remaining flaws in the Tcl/Tk Port) not yet on Windows 3.1. Once the Tcl/Tk port from SUN is bugfree, this version should work without change on any platform.
There have been many cosmetic improvements to both Spin and Xspin, and a small number of extensions (`mtype,' for instance, is now a fully supported data-type in Promela ; -DREDUCE is now the default compilation mode ; and `printf' statements are now automatically disabled from any verification model generation by Spin - so that output from printfs does not clutter up your verification runs (unless you want to... check Doc/V2.Updates for details on how to override some or all of this).

Some Recent Papers

Appendix - SPIN96 CFP

SPIN96, Second International SPIN Verification Workshop

Date:     Monday, August 5, 1996
Place:    Rutgers University, New Brunswick, New Jersey, USA
Duration: One day (tentatively: 9am - 5pm)

Keynote speaker: Moshe Y. Vardi, Rice University

Papers: Papers can be up to 20 pages in length and can be
        either a report on work in progress or a regular
        research paper on work that is somehow related to
        the SPIN system.

Demos:  Tool demonstrations, of extensions, restrictions
        variations, or alternatives, to SPIN, are invited.
        Please tell us as early as possible if you plan
        to demonstrate software - so that we can make sure
        we can set it up properly and make it work.

Dates:  The deadline for all contributions is:
                Saturday, June 15, 1996.
        Papers can be submitted electronically, in PostScript
        form to any one of the organizers.  We will make available
        a Proceedings of the workshop in both printed and also, for
        the authors that permit us to do so, in electronic form.
        The final workshop Proceedings will be published in book
        form by the AMS in the regular DIMACS series.

Organizers:
        Jean-Charles Gre'goire - [email protected]
        Gerard J. Holzmann     - [email protected]
        Doron Peled            - [email protected]
End of Appendices.

End of Newsletter Nr. 10.

Gerard J. Holzmann ([email protected])