Formally understanding Rust’s ownership and borrowing system at the memory level - Kan, Shuanglong; Chen, Zhe; Sanán, David; Liu, Yang (Formal Methods in System Design: An International Journal, 2024)