Erlang’s powerful communication model allows us to build high-level concurrent systems. These can, however, harbour subtle communication errors less severe than global deadlock or crashes. We believe that some of these errors can be quickly detected with static analysis. To facilitate detection of these errors, we have built a tool intended to be usable by developers. The tool has been created with certain design principles in mind, aiming for usability and maintainability.

We present a fragment of Erlang’s type system, a subtyping relation for it, and our type inference functions for communicating portions of Core Erlang. The implementation of the tool is detailed, noting specific behaviours and oddities encountered when dealing with Core Erlang code generated by the Erlang/OTP compiler, some of which complicate our analysis.

The current state of the tool is discussed, and we show examples of the subtle communications errors that the tool can detect. Although the preliminary version of our tool is basic and somewhat reliant on user input due to our lack of control- or data-flow analyses, we believe it serves as a useful foundation for automatic verification of Erlang concurrency on an ad-hoc basis.

PhD Candidate in the School of Computing.