SPIN NEWS - Nr. 14 - September 22, 1996

Contents of this NewsLetter:

SPIN96 Workshop Proceedings

The second SPIN workshop, held 5 August 1996 at Rutgers University, attracted about 50 people (up from 29 people at our first workshop in Montreal 1995). The workshop was opened by DIMACS Director Fred Roberts, and began with an inspiring keynote presentation by Prof. Moshe Vardi, reviewing the automata-theoretic foundation for LTL model checking. As planned, a total of 4 demos were given during the workshop, of extensions of the basic SPIN system:

More information on those extensions is available from the authors of each tool directly.

The preprints of most of the papers that were presented at the workshop can be found at the url:

A more formal volume with the proceedings is scheduled to be printed by the American Mathematical Society (to appear sometime early next year).

SPIN97 Workshop Announcement

The good news is that there will be a Third Spin Workshop in 1997. The Workshop will be organized at Twente University immediately following the TACAS97 Workshop, also held there. A first announcement and preliminary call for papers can be found at:

As before, the workshop will be a forum for discussing and sharing experiences with the Spin model checker, a meeting place for all those who work on (1) the theoretical foundation of computer aided verification, on (2) the application of model checkers such as Spin to problems of practical significance, on (3) empirical studies of the relative effectiveness of different types of search algorithms and memory management techniques for model checking, and on (4) significant extensions or modifications of the basic system.

SPIN97 we will also have a distinguished keynote speaker. We are very pleased that Prof. Pierre Wolper from the University of Liege, who together with Moshe Vardi is one of the main contributors to the theory on which SPIN is founded, has accepted our invitation to be an invited speaker.

The important details on SPIN97 are:

     When    :  Saturday, 5 April 1997
     Where   :  Twente University (the site of TACAS97)
     Deadline:  Saturday, 15 February 1997
                (for all contributions, and demo proposals)
     Program Committee:
                Rom Langerak       - [email protected]
                Eli Najm           - [email protected]
                Gerard J. Holzmann - [email protected]
     Keynote Presentation:
                Prof. Pierre Wolper - [email protected]

Spin Updates since the last NewsLetter

Since July 5, the date of the last Spin NewsLetter, there have been two updates of the Spin sources. The current version number is 2.9.1 dated 16 September 1996. The most important change remains largely invisible: instead of a special-purpose algorithm for checking the existence of non-progress cycles, Spin now compiles in a predefined LTL formula for capturing non-progress as a standard Buchi acceptance property (the formula <>[] np_ ). The advantage is that Spin now has a single unified formal automata theoretic framework; a small disadvantage is what appears to be a small increase in the size of the state spaces that are generated for non-progress cycle detection.

The graphical front-end to Spin (XSPIN) was updated with more menu selections to take advantage of some of the more recent additions to Spin, such as the search for shortest error trails.

The precompiled version of Spin for PC's now also supports the more recent releases of the Gnu C compilers, and the sources were purified a little to prevent compiler warnings.

The Next operator was added to the translation algorithms from LTL to Buchi Automata - but by default this option is not enabled in the Spin executables. (For partial order reduction to work correctly, the Never Claims that are generated from LTL formulae must be closed under stuttering - this rules out the use of the Next operators in those cases.) To enable the operator, it suffices compile the Spin sources with an extra directive -DNXT

Two new tutorial-style documents were added to the Doc directory of the Spin distribution:

which can walk a first-time Spin user through the first verification session with Xspin, and
which gives a more advanced user lots of interesting verification exercises to work with. The Promela code for the exercises is also included in machine readable form (as a shell-archive) as:

APPENDIX: AAS Workshop in Paris

An interesting new SIGPLAN workshop on the Automated Analysis of Software (AAS) is being organized in Paris, France. The url for the workshop is:

From the call for papers:
The subject of the workshop is model-based automatic analysis and its role in the design and development of software. By 'model-based', we mean first, that an abstract model is analyzed in place of the software artifact itself, and second, that automatic analyses based on semantic models-such as model checking or state exploration-are used rather than syntax-driven proof techniques.
Topics of interest include:
     -analysis algorithms and tools
     -modeling notations and methods
     -extraction of models from artifacts
     -construction of artifacts from abstract models
     -techniques for decomposition and abstraction of models

Important Dates
     Oct 18, 1996  *  Submission deadline
     Nov 17, 1996  *  Notification of acceptance or rejection
     Dec 16, 1996  *  Final versions due
     Jan 14, 1997  *  Workshop

Workshop chairs:
	Rance Cleaveland - [email protected]
	Daniel Jackson   - [email protected]

End of Newsletter Nr. 14.

Gerard J. Holzmann ([email protected])