Revisiting Borrow Checking with Abstract Interpretation.

The prevalence of memory safety vulnerabilities in contemporary software systems has made the adoption of memory-safe programming languages increasingly critical.Among the available options, borrow checking, introduced by the Rust programming language, offers a compelling balance between safety and performance by enforcing disciplined ownership and reference semantics at compile time.However, further formalisation and refinement of the underlying framework is necessary, particularly to enhance its precision in the presence of flow-sensitive programming patterns.In this paper, 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.We formalise the syntax and operational semantics of the IR and develop a sound type system that enforces origin-based constraints on references.Through a series of examples, we show how our framework can successfully validate programs that are rejected by Rust's current implementation due to conservative approximations.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.