Developing reliable concurrent software is a hard task given the inherent non-deterministic nature of concurrent systems. A technique which is often used to check that a concurrent program fulfils a set of desirable properties is model checking. In model checking, all the states of a concurrent system are systematically explored.

We have developed McErlang, a model checker for Erlang. The Erlang program to be analyzed is run under the McErlang run-time system, under the control of a verification algorithm, by the normal Erlang byte-code interpreter. The pure computation part of the code, i.e, code with no side effects, including garbage collection, is executed by the normal Erlang run time system. However, the side effect part is executed under the McErlang run-time system which is a complete rewrite in Erlang of the basic process creating, scheduling, communication and fault-handling machinery of Erlang. Naturally the new run-time system offers easy check pointing (capturing the state of all nodes and processes, of the message mailboxes of all processes, and all messages in transit between processes) of the whole program state as a feature. McErlang has been used to verify critical parts of a number of Erlang applications.

In this talk we will give a brief introduction to McErlang, and give a demo showing how to use the tool in practise.