Subscribe to our Erlang Factory newsletter to receive the latest updates and news

Lars-Ake Fredlund
Erlang researcher and creator of McErlang
Universidad Politécnica of Madrid

Lars-Ãke first learned of Erlang when attending a course on "Declarative Real-Time Programming" at the Royal Institute of Technology in 1991. Working at the Swedish Institute of Computer Science (SICS), the relationship with Erlang continued; one outcome was a formal semantics for Erlang (part of his PhD thesis in 2001). Lured to Madrid in 2005, Lars-Ãke found more free time to work with Erlang resulting in a number of articles concerning the "real" communication guarantees of Erlang (more tricky than you think...) and a cool new tool to verify concurrent Erlang software: McErlang. He also tries, mostly in vain, to convince his office mates and students at the Technical University of Madrid that Erlang has a much better process model than ADA.

Lars-Ake Fredlund is Giving the Following Talks
McErlang, a model checker for Erlang programs

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.