GenMC: Model checking for concurrent C programs

Summary

GenMC is a model checking algorithm for concurrent programs that is parametric in the choice of memory model. Subject to a few basic conditions about the memory model, our algorithm is sound, complete and optimal, in that it explores each consistent execution of the program according to the model exactly once, and does not explore inconsistent executions or embark on futile exploration paths.

We implement GenMC as a tool for verifying C programs under the RC11 memory model. Its performance is comparable to the state-of-art stateless model checkers Nidhugg and RCMC, and in certain cases exponentially faster thanks to its coarse partitioning of executions.

Papers

Implementation

People

Related projects

Imprint | Data protection