Place Capability Graphs

See https://rust-formal-methods.github.io... for more information.

Presenter was Zack Grannan, a PhD student in the Software Practices Lab at the University of British Columbia working under the supervision of Alex Summers. His research focuses on Rust program verification, and he is also involved in the development of the Prusti program verifier.

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 talk, Zack presented Place Capability Graphs: a novel model of Rust's type-checking results, which lifts these limitations, and is directly calculated from the Rust compiler's own programmatic representations and analyses. The PCG model supports almost all real-world Rust code (97% of Rust functions in the most popular public crates), and is suitable as a general-purpose basis for verification and program analysis tools.