Spin: Reducing State Space
Verification is a paramount and formidable challenge in software engineering. Moreover, it serves as a pivotal process that distinguishes software engineering from mere software development. Spin is a popular open-source software verification tool that has seen continuous research and development since its inception at Bell Labs in 1980.1 Under the hood, Spin is an explicit-state model checker, meaning it exhaustively searches the entire state space of a model. To check an algorithm or system using Spin you must first recode it in Promela, a C-like language used for defining a model for use with Spin....