Modular Formal Verification of Rust Programs with Unsafe Blocks

Nima Rahimi Foroushaani, Bart Jacobs

Rust is a modern systems programming language whose type system guarantees memory safety. For the sake of expressivity and performance it allows programmers to relax typing rules t…