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:
The preprints of most of the papers that were
presented at the workshop can be found at the url:
http://netlib.bell-labs.com/netlib/spin/ws96/papers.html
A more formal volume with the proceedings is scheduled to be printed by the American Mathematical Society (to appear sometime early next year).
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:
http://netlib.bell-labs.com/netlib/spin/ws97/call.html
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 - langerak@cs.utwente.nl
Eli Najm - najm@res.enst.fr
Gerard J. Holzmann - gerard@research.bell-labs.com
Keynote Presentation:
Prof. Pierre Wolper - pw@montefiore.ulg.ac.be
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:
Doc/GettingStarted.ps
which can walk a first-time Spin user through the first verification
session with Xspin, and
Doc/Exercises.ps
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:
Test/examples
An interesting new SIGPLAN workshop on the Automated Analysis of Software (AAS) is being organized in Paris, France. The url for the workshop is:
http://www4.ncsu.edu/~rance/aasFrom the call for papers:
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 - rance@csc.ncsu.edu
Daniel Jackson - dnj@cs.cmu.edu
Gerard J. Holzmann (gerard@research.bell-labs.com)