Contents NewsLetter 26 - July 12, 1999:
Spin-5 Proceedings now online
The proceedings of the Fifth Spin workshop, held July 5 in Trento, Italy, are now online. You can find them at:
http://netlib.bell-labs.com/netlib/spin/ws99a/program99.html
You'll see some interesting papers there. John Rushby's keynote focused on synergies between theorem proving techniques and model checking techniques, e.g. for enabling computer aided abstractions for model extraction. We'll try to get the viewgraphs from John's talk online as well.
The important theme of abstraction in model checking returned also in the presentation by Stahl, Baukus, Lakhnech and Steffen (Divide, Abstract, and Model-Check). Two presentations focused on the use of Spin as a model checking engine for the verification of Java applications (Visser, Havelund and Penix), or for the verification of Manifold applications (Fagot, and Scutella). Two papers discussed engineering choices that can enhance the performance of Spin (Geldenhuys and Villiers on alternative ways to encode the Spin statevectors, and Lerda and Sisto reporting on experiments with running Spin safety checks on distributed hardware). Dragan Bosnacki from Eindhoven University reported on a study of the subtle interactions of Spin's weak fairness algorithm with partial order reductions and the semantics of rendez-vous and unless operations. Dragan discovered several anomalies in this study. As Dragan pointed out, some of Spin's current warnings against the use of these combinations could be avoided by a modification of the search algorithms.
Spin-6 Details
The next workshop will be held in Toulouse, France on September 21 and 24 1999. We have had a large number of submissions to this workshop. To accomodate a richer selection of papers we have therefore divided the program over two days. The details of the program can be found at:
http://www.fee.uwaterloo.ca/~sleue/6thSPIN99-prm.html
and the remaining details at:
http://www.fee.uwaterloo.ca/~sleue/6thSPIN99.html
The proceedings of Spin-5 and Spin-6 will appear as a joint LNCS Volume, published by Springer Verlag. We hope to have the final proceedings available at the Spin-6 workshop date.
Spin Version 3.3
Thanks to all who downloaded the first release of 3.3.0. A few small problems were found that have been corrected in 3.3.1. For the time being, we'll also keep the last version of 3.2 on the distribution site, for comparisons and as a backup. Note that all new optimizations in 3.3. can also be disabled at any time by running spin with the -o[1-4] override flags. (You can always type spin -- to see what the various options do.)
A detailed description of the improvements made in 3.3 will be given at Spin-6 in Toulouse.
End of Newsletter Nr. 26.
Spin Homepage, spin_list@research.bell-labs.com