Abstract
This paper describes software tools for teaching concurrency and model checking. JSPIN is an development environment for SPIN that formats and filters the output of a simulation according to the user's specification. SPINSPIDER. uses debugging output from SPIN to generate a diagram of the state space of a PROMELA model, the diagram can be incrementally displayed using IDOT. VN supports teaching nondeterministic finite automata. The ERIGONE model checker is a partial reimplementation of SPIN designed to be easy to use, well structured and well documented. It produces a full trace of the execution of the model checker in a format that is both readable and amenable to postprocessing.