Lars-Åke 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-Åke's University Home Page
- McErlang
- ProTest Project
Lars-Åke Fredlund 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.
