The SPIN Model Checker is used for both teaching software verificationtechniques, and for validating large scale applications. The growing number ofusers has created a need for a more comprehensive user guide and a standardreference manual that describes the most recent version of the tool. This bookfills that need.SPIN is used in over 40 countries. The offical SPIN web site, spinroot.comreceives between 2500 and 3000 hits per day.It has been estimated that up to three-quarters of the $400 billion spentannually to hire programmers in the United States is ultimately spent ondebugging.

Product Description: What is Spin? Spin is a general tool for the specification and formal verification of software for distributed systems. It has been used to detect design errors in a wide range of applications, such as abstract distributed algorithms, data communications protocols, operating systems code, and telephone switching code...read more

Product Description: This book presents surveys on the theory and practice of modeling, specifying, and validating concurrent systems. It contains surveys of techniques used in tools developed for automatic validation of systems. Other papers present recent developments in concurrency theory, logics of programs, model-checking, automata and formal languages theory...read more

(view table of contents)