Clara Benac Earle
Ex-Ericsson CS Lab and model checking expert
Universidad Politécnica of Madrid
Clara was first exposed to Erlang as a student from Spain who got the opportunity to do a master project at Ericsson CSLAB - the birthplace of Erlang. Having seen enough of Sweden, she decided to spread Erlang technology to the UK academy by pursuing a PhD degree at the University of Kent, after which she returned home to Madrid, Spain where she now works at the Technical University of Madrid. Her speciality is model checking Erlang programs, and now works together with other researchers in the European ProTest project on developing new cool Erlang development tools.
Clara Benac Earle 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.
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.
