A primer on model checking
Mordechai Ben‐Ari · ACM Inroads · 2010
Model checking is a widely used formal method for the verification of concurrent programs. This article starts with an introduction to the concepts of model checking, followed by a description of Spin, one of the foremost model checkers. Software tools for teaching concurrency and nondeterminism using model checking are described: Erigone, a model checker for teaching; jSpin, a development environment; VN, a visualization of nondeterminism.