SPIN NEWSLETTER Nr. 17

Contents NewsLetter 17 - 21 March 1997:



SPIN97 keynote

Many have already signed up for the SPIN97 workshop in Twente two weeks from now. Registration and participation is free. To help plan for the right number of chairs and lunches, however, please send a note to Rom Langerak if you plan to come and have not yet send in a registration:

	[email protected]
The keynote presentation at the SPIN97 workshop is by Pierre Wolper, together with Moshe Vardi responsible for defining the formal automata theoretic framework for verification that underlies Spin. Below is the abstract for Pierre's talk on April 5. We hope to see you all at the workshop!
                      Where could SPIN go next?
       A unifying approach to exploring infinite state spaces

                            Pierre Wolper
                         University of Liege

Starting with the observation that many verification problems can be
reduced to deciding various forms of state reachability, this talk
then examines how the latter can be done in the context of infinite
state systems. It identifies the central problem to be solved as
computing, in a way that can generate an infinite number of states in
a finite amount of time, the fixpoint of the (forwards or backwards)
transition relation of the program to be analyzed. Doing this
requires three basic components: a finite representation for infinite
sets of states together with the algorithms for manipulating it; a
technique for bootstrapping from finite to infinite sets of states;
and a termination criterion. For the first component, its is shown
that regular sets play a central role. For the second, a variety of
techniques are discussed, but one, the "loop-first search", is
emphasized. For the third, it is argued that termination detection is
sufficient and that termination guarantee offers little additional
practical advantage beyond a theoretical illusory peace of mind.

SPIN96 Proceedings

The proceedings of the 1996 Spin Workshop are now listed on the home page of the AMS as Volume DIMACS/32 (i.e., not DIMACS/39 as we thought before). See http://www.ams.org/bookstore/ and follow the links for 'Books' and 'What's New'

The book is expected to be ready for shipping by early May (sadly, not in time to be available at this year's workshop.) The volume for the Partial Order Methods workshop (DIMACS/29) has been published and was said to be available by mid March.

Formal Methods Applications Database

There is a formal methods applications database at URL: http://www.csr.ncl.ac.uk/projects/FME/InfRes/applications/index.html
If you have a significant application of Spin, you can consider submitting the information for inclusion in this database. There is a form available at the above URL. For more information contact the maintainer of the database, [email protected]

Spin Version 2.9.6

The current version of Spin is 2.9.6. It has a thoroughly revised (and much improved) version of the Collapse compression mode, as promised in Newsl. 15 and described in the Spin97 workshop paper. Xspin has also been updated to work correctly with the last stable release of Tcl/Tk 7.6/4.2. (Be warned not to try it yet with the alpha releases 8.0, it's known to break.)

There is also a new version of the pc_spin296.zip file that contains a 32-bit executable. The new Tcl/Tk actually cares about this when you run Spin on the PC (the older versions can hang up your system during simulations.)

API Question

Il-Hyung Cho asks:

    From cs.clemson.edu!ihcho Sun Mar  2 20:08:03 EST 1997
    From: cs.clemson.edu!ihcho (Il-Hyung Cho)
    Subject: API for SPIN?
  
    Is there an API (Application Programming Interface) exists
    for the SPIN tool?  Does SPIN provide an interface that my
    C++ or Java program can work with?
If anyone has written such an API, please send us a note.

Spin Related URLs

Some interesting places to check out:

Some Recent Papers

End of Newsletter Nr. 17.

Gerard J. Holzmann ([email protected])