Spin is a tool for software model checking. It was written by Gerard J. Holzmann and others, and has evolved for more than 15 years. Spin is a automata-based model checker, as it represents the negated LTL property it checks the model against by a Büchi automaton. It then performs a depth-first search for the recurrent reachability of an accepting state of the product automaton. If there exists some path that reaches this accepting state infinitely often, it serves as a counterexample.
Spin offers a large amount of options to speed up the checking process and save memory, like
- partial order reduction
- state compression
- bitstate hashing (instead of storing whole states, only their hash code is remembered in a bitfield; this saves a lot of memory but voids completeness)
- weak fairness enforcement
Spin does not perform the model checking itself but generates C sources for a problem-specific model checker. This rather antique technique saves memory and speeds things up, and also allows to directly insert chunks of C code into the model.
External links
Spin home page