RustMC: Extending the GenMC stateless model checker to Rust

Oliver Pearce, Julien Lange, Dan O'Keeffe

RustMC is a stateless model checker that enables verification of concurrent Rust programs. As both Rust and C/C++ compile to LLVM IR, RustMC builds on GenMC which provides a verifi…