Ebook: The spin model checker : primer and reference manual

1. Finding Bugs in Concurrent Systems -- 2. Building Verification Models -- 3. An Overview of PROMELA -- 4. Defining Correctness Claims -- 5. Using Design Abstraction -- 6. Automata and Logic -- 7. PROMELA Semantics -- 8. Search Algorithms -- 9. Search Optimization -- 10. Notes on Model Extraction -- 11. Using SPIN -- 12. Notes on XSPIN -- 13. The TimeLine Editor -- 14. A Verification Model of a Telephone Switch -- 15. Sample SPIN Models -- 16. PROMELA Language Reference -- 17. Embedded C Code -- 18. Overview of SPIN Options -- 19. Overview of PAN Options -- App. A. Automata Products -- App. B. The Great Debates -- App. C. Exercises with SPIN -- App. D. Downloading SPIN