McErlang: A Model Checker for a Distributed Functional Programming Language

We present a model checker for verifying distributed programs writtenin the Erlang programming language. Providing a model checker forErlang is especially rewarding since the language is by now being seenas a very capable platform for developing industrial strengthdistributed applications with excellent failure tolerancecharacteristics. In contrast to most other Erlang verificationattempts, we provide support for a very substantial part of thelanguage. The model checker has full Erlang data type support, supportfor general process communication, node semantics (inter-processbehave subtly different from intra-process communication), faultdetection and fault tolerance through process linking, and can verifyprograms written using the OTP Erlang component library (used by mostmodern Erlang programs).As the model checking tool is itself implemented in Erlang we benefitfrom the advantages that a (dynamically typed) functional programminglanguage offers: easy prototyping and experimentation with newverification algorithms, rich executable models that use complex datastructures directly programmed in Erlang, the ability to treatexecutable models interchangeably as programs (to be executed directlyby the Erlang interpreter) and data, and not least the possibility tocleanly structure and to cleanly combine various verificationsub-tasks. In the paper we discuss the design ofthe tool and provide early indications on its performance