Model checking software

Since 1995, SPIN workshops have been held annually in various locations, including Montreal, New Brunswick, Enschede, Paris, Trento, Toulouse, Stanford, Toronto, Grenoble, and Portland. Most workshops have been organized as satellite events of larger conferences such as CAV, TACAS, FORTE/PSTV, FLOC, the World Congress on Formal Methods, FMOODS, ICSE, and ETAPS. This year, SPIN was again held alongside ETAPS 2004. The co-location with conferences has successfully broadened the reach of SPIN model checking technology. Since 1999, the proceedings have been published in Springer-Verlag’s Lecture Notes in Computer Science series. The ongoing success of SPIN workshops reflects the maturation of model checking technology, expanding beyond hardware to software applications. Initially focused on algorithms and tool development for the SPIN model checker, the workshops have evolved to encompass a wider range of software model checking techniques, tools, and applications. The SPIN workshop has established itself as a key forum for practitioners and researchers interested in model checking techniques for validating and analyzing communication protocols and software systems.