ICFP/SPLASH 2025 (series) / Erlang 2025 (series) / Erlang 2025 /
Mechanised Proofs of Atom Exhaustion in Erlang
This program is tentative and subject to change.
Sun 12 Oct 2025 11:00 - 11:38 at Seminar Room 7 - Formal Semantics & Verification Chair(s): Daniel Gorin
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.
This program is tentative and subject to change.
Sun 12 OctDisplayed time zone: Perth change
Sun 12 Oct
Displayed time zone: Perth change
11:00 - 12:30 | |||
11:00 38mTalk | Mechanised Proofs of Atom Exhaustion in Erlang Erlang Arsenii Fomin Eötvös Loránd University, Péter Bereczky Eötvös Loránd University, Dániel Horpácsi Eötvös Loránd University, Gergő Lajos Turán Eötvös Loránd University | ||
11:38 37mTalk | Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang Erlang Gergő Lajos Turán Eötvös Loránd University, Arsenii Fomin Eötvös Loránd University, Péter Bereczky Eötvös Loránd University, Dániel Horpácsi Eötvös Loránd University, Simon Thompson University of Kent (UK) | ||
12:15 15mTalk | (Lightning Talk) The State of The Unions: challenges for type-checking unions and generics at WhatsApp Erlang Maxwell Heiber Meta |