The Rust programming language is famous for its strong ownership regime: at each point, each value is either exclusively owned, exclusively borrowed through a mutable reference, or borrowed as read-only through one or more shared references. These rules, known as Rust's pointer-aliasing rules, are exploited by the Rust compiler to generate more efficient machine code, and enforced by Rust's static type system, except inside unsafe blocks. In this paper, we present our work in progress towards the first program logic for modularly verifying that Rust programs that use unsafe blocks comply with the pointer-aliasing rules.

翻译：Rust编程语言以其严格的所有权机制而闻名：在每个时间点，每个值要么被独占拥有、要么通过可变引用被独占借用、要么通过一个或多个共享引用作为只读借用。这些规则（即Rust的指针别名规则）被Rust编译器用于生成更高效的机器码，并通过Rust的静态类型系统强制执行——但unsafe块内部除外。本文介绍了我们正在开展的研究工作，旨在构建首个用于模块化验证使用unsafe块的Rust程序是否符合指针别名规则的程序逻辑。