NewsLetter 37 - June 9, 2003:
Spin/Xspin Version 4.0.6The current version of both Spin and Xspin is 4.0.6.
There have been a number of extensions in functionality in the newer versions of Spin, apart from the support for embedded C code. (As well as a few subtle bug fixes, the last one in the implementation of the weak-fairness algorithm. An up to date of all changes in the code is always available in the Doc/V4.Updates file, which is part of the main distribution file spin406.tar.gz.)
Breadth-First Search One of the more interesting ones is the implementation of the Breadth-First Search option. As can be expected, this option uses more memory than Spin's traditional depth-first search, but it finds shorter counter-examples. It works for all safety properties, including those specified in LTL. The verifier will switch to the breadth-first search mode when compiled with directive -DBFS. The corresponding option can also be set in the verification options panel of the newer versions of xspin.
PreProcessing Checks Also new option in spin is the command line option -I, which can be used to reproduce a version of the input after all preprocessing and inlining was performed. The reproduced code omits declarations and proctype parameter lists and it will include some internally generated labels and jumps (e.g., those replacing break statements). The option is very useful to debug the precise effect of all inline definitions and preprocessor macros.
Xspin There is also a new version of xspin on the website (xspin406.tcl) that fixes some long-standing problems (courtesy of Margaret Smith), as well as some small bugs. For instance:
Online Workshop ProceedingsThe proceedings of the 10th Spin Workshop are online at
http://spinroot.com/spin/Workshops/ws03/program2003.htmlThe online proceedings of all previous workshops also remain available, see the list at the bottom of the main Spin homepage: http://spinroot.com/spin/whatispin.html
Note also the announcement for the next, 11th, Spin Workshop, which will be held April 1-3, 2004 in Barcelona, Spain, co-located with ETAPS 2004, and organized by Susanne Graf and Laurent Mounier from Verimag.
http://www-verimag.imag.fr/SPIN-2004/cfp.htmlThe submission deadline for this workshop is December 6, 2003.
The New BookA publication date for the new Spin book has now been set and the ISBN number is now known. It should be available in stores by mid August 2003. The table of contents for the final draft of the book can be found online at: http://spinroot.com/spin/Doc/Spin2003_TOC.pdf. These are the details:
The Spin Model Checker Primer and Reference Manual. Gerard J. Holzmann Addison-Wesley ISBN 0-32122-862-6 approx. 600 pgs.
End of Newsletter Nr. 37.
To subscribe/unsubscribe: [email protected]