Lars-Ake Fredlund
Erlang researcher and creator of McErlang
Technical University 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' University Home Page
- McErlang
- ProTest Project
Lars-Ake Fredlund is Giving the Following Talks
The McErlang model checker
In this 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).
In addition to the Tutorial, there will also be a Hands-on session where Clara Benac Earle will be covering the basics of the McErlang tool. This will allow delegates to install the tool and try it out with the help of some exercises.
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).
In addition to the Tutorial, there will also be a Hands-on session where Clara Benac Earle will be covering the basics of the McErlang tool. This will allow delegates to install the tool and try it out with the help of some exercises.
