Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions

Wannes Tas, Bart Jacobs

The Rust programming language is famous for its strong ownership regime: at each point, each value is either exclusively owned, exclusively borrowed through a mutable reference, or…