Publications

2025

1. BSc Thesis

   

   A Rust Frontend for GenMC

   Arbenit Kamberi

   Aug 2025

   Abs Bib HTML PDF

   Stateless model checkers are widely used for verifying concurrent programs, but their application to Rust has thus far been limited. Existing model checkers lack full support for aspects of Rust’s memory model, which prevents accurate verification of concurrent Rust programs. In this thesis, we extend GenMC, a state-of-the-art model checker for concurrent C/C++ programs that supports various weak memory models and is optimal in the number of executions explored, to also verify Rust programs. GenMC verifies the LLVM-IR produced during compilation of a C/C++ program. We extend it to support various constructs in LLVM-IR generated by the Rust compiler and develop approaches for overcoming the challenges we faced in doing so. We provide custom implementations of Rust’s standard library concurrency APIs so they can be used with GenMC. We successfully ran and compared a collection of tests in Rust with the corresponding output for the same test in C. As a case study, we verified various concurrent data-structures of a popular, open-source Rust crate. Our work enables the automatic verification of Rust programs and provides a great foundation for future extension to more concurrency primitives in Rust.

   @mastersthesis{kamberi2025rustgenmc,
     title = {A Rust Frontend for GenMC},
     author = {Kamberi, Arbenit},
     school = {ETH Zurich},
     type = {Bachelor's thesis},
     address = {Zurich, Switzerland},
     year = {2025},
     month = aug,
     keywords = {Model checking, Concurrency, Rust, LLVM, Compilers},
   }