This book constitutes the refereed proceedings of the 5th and 6th international SPIN workshops on SPIN Model Checking, held as a satellite workshop of the Federated Logics Conference, FLoC'99, in Trento, Italy, July 1999, and as a user group meeting at the Formal Methods World Congress, FM'99, in Toulouse, France, in September 1999 respectively. Finite-state model checking, as it is supported by the explicit-state model checker SPIN, is enjoying constantly increasing popularity in automated property validation of concurrent, message based systems. This book presents up-to-date research results centered around SPIN as well as valuable surveys and summaries of application experience.