RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code.

Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer

Browse the full PLDI paper archive.