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 Linear Temporal Logic 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:

SPIN does not perform the model checking itself but generates C programming language 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.

=Book=

*Holzmann, G. J., The SPIN Model Checker: Primer and Reference Manual . Addison Wesley, 2004. ISBN 0-321-22862-6.

=External links=