Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing(…)
summary
Place Capability Graphs (PCG) present a concretely computable model of Rust ownership that is extracted from the compiler’s MIR and borrow-checker facts and encodes lifetime projections, MIR/borrow-checker facts, and path-sensitive capabilities per program point. The implementation generates annotations consumed by verifiers, models over 97% of Rust functions in top crates, produces 7 million mutants with almost all rejected by rustc, and plugs into Flowistry and Prusti as a reusable crate that simplifies and extends those tools.
AI-written summary · about
chapters (11)
- 0:00Rust ownership basics
- 2:06Modeling ownership challenges
- 3:31Desired model properties
- 4:56Introducing Place Capability Graphs
- 5:37How PCGs work
- 6:38PCG advanced features
- 7:20PCG evaluation on Rust code
- 8:22PCGs vs Rust compiler
- 9:25PCGs in analysis tools
- 11:12Conclusion and future
- 11:34Q&A
related talks
56mVisualizing and Explaining Rust's Ownership Model
19mA Grounded Conceptual Model for Ownership Types in Rust
56mReady for Rust
50mRust's Borrow Checker Proven Correct!
40mAgainst Borrowing: Own the forest, not the trees!
59mRust for C++ developers - What you need to know to get rolling with crates
28mYou Don't Own Me
40mWhy Rust?