To verify properties of the code, the tool first translates the Erlang code into a process algebraic specification. The outcome of the translation is made more efficient by taking advantage of the fact that software written in Erlang builds upon software design patterns such as client–server behaviours. A labelled transition system is constructed from the specification by use of the CRL toolset. The resulting labelled transition system is model checked against a set of properties formulated in the -calculus using the Caesar/Aldébaran toolset.

As a case study we focus on a simplified resource manager modelled on a real implementation in the control software of the AXD 301 ATM switch. Some of the key properties we verified for the program are mutual exclusion and non-starvation. Since the toolset supports only the regular alternation-free -calculus, some ingenuity is needed for checking the liveness property non-starvation. The case study has been refined step by step to provide more functionality, with each step motivated by a corresponding formal verification using model checking .