SPIN is the world's most popular, and arguably one of the world's most powerful, tools for detecting software defectsin concurrent system designs. Literally thousands of people have used SPIN since it was first introduced almost fifteenyears ago. The tool has been applied to everything from the verification of complex call processing software that isused in telephone exchanges, to the validation of intricate control software for interplanetary spacecraft.