Revisiting Borrow Checking with Abstract Interpretation
By: Aurélien Coet, Didier Buchs
Abstract
We propose a novel reinterpretation of Rust's borrow checking mechanism as a form of abstract interpretation over a dedicated intermediate representation (IR). Our methodology captures the aliasing and initialisation properties of variables through the construction of abstract program traces that enable fine-grained, path-sensitive verification of memory safety properties. By decoupling borrow checking from Rust's surface syntax and embedding it within a language-agnostic IR, our work lays the foundation for integrating Rust-style memory safety into a broader class of programming languages and compiler infrastructures.
Keywords
Borrow Checking, Abstract Interpretation, Memory Safety, Intermediate Representation
Cite as:
AurĂ©lien Coet, Didier Buchs, “Revisiting Borrow Checking with Abstract Interpretation”, Journal of Object Technology, Volume 25, no. 1 ( 2026), pp. 1:1-16, doi:10.5381/jot.2026.25.1.a14.
DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn