Arbenit Kamberi

My camel and I in Morocco🐫

I’m a Computer Science master’s student at ETH Zurich, working on program verification, automated reasoning, and computer vision. My major is Secure and Reliable Systems and my minor is in Computer Vision. Within the major I take essentially every course ETH offers on verification and reasoning: mechanised PL metatheory, model checking, and deductive program and protocol verification.

My Bachelor’s thesis built a Rust frontend for GenMC, a state-of-the-art stateless model checker for concurrent programs, so that it can verify Rust’s compiled LLVM-IR, advised by Michalis Kokologiannakis. Recently, I worked with Michalis again on improving GenMC’s consistency checker. I’m currently a research intern at the VERSE Lab at NUS, working with Ilya Sergey on LTL model checking. Before that, I spent a computer vision internship rebuilding a video-analysis pipeline for industrial defect detection.

I was also a teaching assistant for ETH’s undergraduate Visual Computing course. My work has centred on reasoning over concurrent and distributed behaviour, and on the compiler toolchains verification runs through. High-performance computing is a side interest I follow alongside, a natural neighbour to that work and to the GPU side of computer vision. What draws me to a problem is when the theory has to hold up against a real workload. My projects and CV have more detail.

news

Aug 28, 2026	Welcome to my new personal website!

selected publications

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}, }