Mechanised Proofs of Atom Exhaustion in Erlang

Static analysis tools aid in developing secure software, but they often produce false positives that undermine developer trust. Formal methods can help validate such findings, provided that the vulnerabilities are precisely formalised. This study presents a formalisation of the atom exhaustion vulnerability within the context of the sequential subset of an existing Core Erlang formal semantics. A sound and complete calculus is proposed to support structured reasoning about the presence of the atom exhaustion vulnerability in Erlang programs. All the results of this paper are implemented in the Coq proof assistant.