Clara Benac Earle
Ex-Ericsson CS Lab and model checking expert
Technical University 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
Tutorial - McErlang
In this 90 minute tutorial Lars-Ake Fredlund will introduce the
McErlang model checking tool for verifying Erlang programs, and examine
some case studies where the tool has been successfully applied.
Model checking is a verification technique where the all the states of a program are systematically explored and checked against correctness properties. Although very effective in hardware verification, there are a number of problems when applying model checking to software:
- Need for abstraction: to use a model checking tool it is often necessary to abstract the source code, almost never is the full source language supported.
- State spaces are too large for model checking algorithms to work.
In the design of the McErlang model checker for Erlang we have addressed both these problems. The language supported is full Erlang, with normal datatypes, processes, nodes, links, monitors, and so on. Moreover its verification algorithm provide some answers even when state spaces are huge (becoming more similar to testing).
Following this introduction, Clara Benac-Earle will provide a hands-on demonstration of the tool. Delegates will be shown how to install it onto their laptops and then they will be taken through some exercises to demonstrate its usage.
Model checking is a verification technique where the all the states of a program are systematically explored and checked against correctness properties. Although very effective in hardware verification, there are a number of problems when applying model checking to software:
- Need for abstraction: to use a model checking tool it is often necessary to abstract the source code, almost never is the full source language supported.
- State spaces are too large for model checking algorithms to work.
In the design of the McErlang model checker for Erlang we have addressed both these problems. The language supported is full Erlang, with normal datatypes, processes, nodes, links, monitors, and so on. Moreover its verification algorithm provide some answers even when state spaces are huge (becoming more similar to testing).
Following this introduction, Clara Benac-Earle will provide a hands-on demonstration of the tool. Delegates will be shown how to install it onto their laptops and then they will be taken through some exercises to demonstrate its usage.
