一句话：提出 Place Capability Graphs，从 Rust 编译器表示直接提取所有权/借用保证，覆盖超 97% 公开 crate 函数，并支撑验证与分析工具。
Rust 的类型系统为控制别名与可变性提供了丰富保证，但现有模型要么针对脱离真实代码的简化语言，要么在精确建模借用、复合类型中的借用、函数签名与循环时存在严重局限。本文提出 Place Capability Graphs，一种对 Rust 类型检查结果的新模型，克服上述限制，并可直接从 Rust 编译器自身的程序化表示与分析中计算得到。评估表明，该模型支持最流行公开 crate 中超过 97% 的 Rust 函数；作者还基于它开发了 Flowistry 与 Prusti 的新原型版本，证明其可作为验证与程序分析工具的通用基础。
Rust’s novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability. However, fully understanding, extracting and exploiting these guarantees is subtle and challenging: existing models for Rust’s type checking either support a smaller idealised language disconnected from real-world Rust code, or come with severe limitations in terms of precise modelling of Rust borrows, composite types storing them, function signatures and loops. In this paper, we present Place Capability Graphs : a novel model of Rust’s type-checking results, which lifts these limitations, and which can be directly calculated from the Rust compiler’s own programmatic representations and analyses. We demonstrate that our model supports over 97% of Rust functions in the most popular public crates, and show its suitability as a general-purpose basis for verification and program analysis tools by developing promising new prototype versions of the existing Flowistry and Prusti tools.
@article{paperbot2921,
title = {Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees},
author = {Zachary Grannan and Aurel Bílý and Jonáš Fiala and Jasper Geer and Markus de Medeiros and Peter Müller and Alexander J. Summers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763122}
}