Mechanised Proofs of Atom Exhaustion in Erlang
summary
Formalisation encodes atom creation as labelled side effects in a Core Erlang small‑step semantics and defines vulnerability as exceeding the atom table limit (default 2^20 ≈ 1,048,576); a GANA calculus proves “generates at least n unique atoms” so the hard conjunction in Coq becomes an automatable proof obligation. Mechanised soundness and completeness connect GANA to atom‑exhaustion, proofs are implemented in Coq (Rocq), demonstrated on a toy that needs 3 atoms to overflow a limit of 2, and the approach scales toward concurrent layers.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:04Formal semantics for languages
- 3:56Coralang with Rock benefits
- 5:00Coralang semantics overview
- 8:58Semantic configurations and rules
- 14:16Atom exhaustion in BEAM
- 17:15Side effects in Coralang
- 21:15Approaches to atom exhaustion
- 26:58GANA calculus intro
- 29:28GANA soundness and completeness
- 31:14Vulnerable program example
- 34:34GANA future extensions
- 36:47Closing remarks
- 37:09Q&A: Extending GANA
- 38:14Q&A: Coralang completeness
related talks
31mSequential Composition of Rational Proofs
27mProofs of proofs: incremental verifiability from recursion and accumulation
01h 17mProof-Carrying Code For the Age of AI: Machine-Checked Guarantees from(…)
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs
12mAutomated Synthesis of Verified Firewalls
25mSuccinct Proofs in Ethereum
30mPractical Zero Knowledge Proofs
58mAutomating Relational Verification of Infinite-State Programs