Spin

Spin is a Tk graphical front end for NMR spectrum simulator (Linux, Windows).

          http://www.sfu.ca/~gay/spin.zip

is a popular open-source software verification tool. It can be used for the formal verification of multi-threaded software applications.

Spin can be used in four main modes:

as a simulator, allowing for rapid prototyping with a random, guided, or interactive simulations
as an exhaustive verifier, capable of rigorously proving the validity of user specified correctness requirements (using partial order reduction theory to optimize the search)
as proof approximation system that can validate even very large system models with maximal coverage of the state space.
as a driver for swarm verification (a new form of swarm computing that can exploit cloud networks of arbitrary size), which can make optimal use of large numbers of available compute cores to leverage parallelism and search diversification techniques, which increases the chance of locating defects in very large verification models.

The source code distribution includes a Tcl/Tk GUI program called iSpin.

Video: [1]