Reasoning about Interior Mutability in Rust using Library-Defined Capabilities

Federico Poli, Xavier Denis, Peter Müller +1

Existing automated verification techniques for safe Rust code rely on the strong type-system properties to reason about programs, especially to deduce which memory locations do not…