A small amount of funds is available to provide financial support for graduate students who would like to attend the workshop, but cannot do so without support. If you'd like to qualify for support for hotel and travel to attend the SPIN96 workshop, please send an application to us as soon as possible, but in any case before Saturday June 15, 1996 at the very latest, attaching a brief supporting statement from your supervisor (email is preferred).
The deadline for paper submissions is June 15 1996. Please note that papers that are included in the DIMACS Proceedings of the workshop must be original contributions, not previously published. Depending on the number of submissions, though, we may consider also other contributions for presentation at the workshop itself, and for inclusion in the (preprint) participants proceedings. Contributions selected for the final DIMACS proceedings will also have to pass a reviewing/editing cycle (following DIMACS rules).
It is probably good to note that
the 1996 Olympic Games in Atlanta will end close to the start
of our workshop (they end on August 3, our workshop is August 5).
The extra flow of travelers may make it hard to make reservations
for flights also in out of New York close to this date...
Make your travel arrangements early!
There are good connections between New York or Newark airport
to New Brunswick (the Rutgers campus where our workshop is held
this year). DIMACS recommends two hotels: the Holiday Inn or
the Comfort Inn. More information:
(or "telnet info.rutgers.edu 90")
SPIN Version 2.8.1
The current version of SPIN (on spinroot.com) contains some important changes:
"<>!p"cannot be satisfied, where "p" is a condition of the form
"process_name[pid]@label_name"(or an arbitrary boolean combination of similar terms).
SPIN version 2.8.1 is also fully compatible with PC's. SPIN itself (a pre-compiled executable is included in the file pc_spin281.zip) works with any operating system (Windows 3.1, Windows NT, or Windows95), provided that you have the gcc executables (shareware) also installed. Xspin, SPIN's Tck/Tk interface works only with Windows95 (there is a bug in Tck/Tk itself when used with Windows 3.1 that does not seem likely to be fixed anytime soon by the Tcl/Tk people).
From the Abstract: This paper presents a case study of the use of model checking for analyzing an industrial protocol, the ACCESS.bus protocol. Our analysis of this protocol was carried out using SPIN, an automated verification system which includes an implementation of model-checking algorithms. A model of the protocol was developed, and properties expressed by linear-time temporal-logic formulas were checked on this model. This analysis revealed subtle flaws in the design of the protocol. Developers who worked on implementations of ACCESS.bus were unaware of these flaws at a very late stage of their development process. We also present suggestions for solving the detected problems.
From the Abstract: In this paper, we carry out an evaluation of three techniques for combatting the state explosion problem in deadlock detection: reachability search with a partial order state space reduction [SPIN], symbolic model checking [SMV], and inequality necessary conditions [INCA]. We justify the method used for the comparison, and carefully analyze several sources of potential bias.
Gerard J. Holzmann ([email protected])