Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees

Zachary Grannan, Aurea Bílá, Jonáš Fiala +4

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…