Erlang and Model Checker "Spin"

[Reto Kramer]

I was wondering if anyone is aware of model checking work done in the
context of Erlang.
It seems that "Spin", the protocol model checker that Gerard Holzmann build
at the Bell Labs allows for very relatively easy transformation from/to
Erlang due to the similar communication models.

Any pointer to previous work in this area is greatly appreciated.

cheers,
- Reto