Spin NewsLetter No. 29

spinnews.gif (1514 bytes)

NewsLetter 29 - July 23, 2000:

Early registration deadline for Spin2000 approaching
Plans for next year's workshop
The next Spin release (3.4.0)

Registration for Spin2000

Please note that the early registration for Spin2000, at Stanford University in California, will expire on August 7. Registration details can be found at:

	
	http://ase.arc.nasa.gov/spin2000/register.html

It will be the first full three-day Spin workshop, in the week before FMOODS2000. We hope to see you all there! The workshop homepage is: http://ase.arc.nasa.gov/spin2000/

Plans for Next Year's Workshop

Plans are underway for the organization of next year's workshop. Matt Dwyer (dwyer@cis.ksu.edu) from Kansas State University will organize it, together with Marsha Chechick (chechik@cs.toronto.edu) from Toronto University. The workshop will be co-located with ICSE2001, which is held in Toronto in May 2001: http://www.csr.uvic.ca/icse2001/. This puts the submission deadline for papers most likely in January of 2001, just five months from now. Stay tuned for more details. Abstracts are due to the ICSE2001 conference itself by August 14. The Spin2001 workshop homepage is

	
	http://www.cis.ksu.edu/santos/spin2001.

The Next SPIN Release (3.4.0)

The current release of Spin is stil 3.3.10. We are working on the next version though. There will be two significant changes in Spin version 3.4.0.

The first is the inclusion of Kousha Etessami's (kousha@research.bell-labs.com) algorithm for the conversion of LTL formula to Buchi automata. The translation to C was done by Reba Schuller. We will include the new algorithm as an option, so that it's performance may be compared with the existing version. (Kousha's algorithm generally produces smaller automata, and runs faster than the current algorithm.
The second change will be the inclusion of a program slicing algorithm that can identify those portions of a model that are redundant for the correctness properties that are stated in assertions and/or in a never claim or LTL formula. The slicing option will produce a series of sugesstions to the user about portions of the model (processes, statements, and data objects) that can be omitted without risk, and with a potential reduction in verification complexity.

We hope to release Spin 3.4.0 in early September.

End of Newsletter Nr. 29.

Spin Homepage, spin_list@research.bell-labs.com