SpinRCP is an integrated development environment for model checking with the Spin model checker. It is used for the verification of concurrent and distributed systems. It offers user friendly editing of the system model, different specifications forms of required model properties, graphical representation of processes in form of non-deterministic finite automata, execution of three types of simulation with the message sequence chart plotting and formal verification of the model. SpinRCP is freely available for 32-bits and 64-bits operating systems such as Windows, Linux and Mac OS X.