GenMC is a stateless model checker for concurrent programs written under the
SC [Lamport 1979],
TSO [Owens et al. 2009],
RA [Lahav et al. 2016],
RC11 [Lahav et al. 2017],
and IMM [Podkopaev et al. 2019] memory models.
It primarily targets C/C++ and Rust programs, verifying safety properties by analyzing
their concurrency patterns (e.g., usage of C11 atomics or Rust's std::sync).
It employs an effective dynamic partial order reduction technique
[Kokologiannakis et al. 2019, Kokologiannakis et al. 2022] that
is sound, complete, and optimal.
GenMC operates at the level of LLVM Intermediate Representation (LLVM-IR).
It uses clang to translate C/C++ programs and rustc to translate Rust programs
into LLVM-IR. This intermediate approach allows GenMC to be language-agnostic regarding
its core verification logic, though it relies on language-specific frontends for
translation.
GenMC should compile on Linux and MacOS provided that the relevant dependencies are installed (see README.md).
For feedback, questions, and bug reports please send an e-mail to michalis.kokologiannakis@inf.ethz.ch.