Model checking with Spin

Spin is a model checker, see Rob Gerth's Short Manual.

On the system you call Spin with its X-interface as "xspin &". Here is also some local material, without pretentions.

1. Introduction to the model checker Spin
2. Verifying LTL formulas
3. A queuing semaphore for mutual exclusion
4. Two different treatments of the Berman-Garay protocol on Byzantine Agreement: a distributed and a sequential version. Compare memory requirements and execution times.
5. Spin Assignments