Reproduce “Verified Implementation of the Next-gen Borrow Checking Algorithm for Rust via Abstract Interpretation” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Jinhua Wu, Yuting Wang, Zhemin Chen
The authors formalize Polonius as a forward abstract interpretation that tracks approximate borrow relationships and connect it to a concrete semantics of references. For Core MIR, they prove that accepted programs cannot access references to freed memory, assuming type, initialization, and move checks. Their implementation matches rustc’s Polonius checker on 499 of 510 selected programs (97.8%), not full compiler equivalence.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.