PV5 GenMCgiven a C program with assertions and a memory model spec, reports safety errors

LLVM-based stateless model checker (SMC) for concurrent C/C++ programs

Application domain/field

Type of tool

Model checker

Expected input


.c file

Expected output

Any safety error that are detected will be reported. These errors can include data races on non-atomic variables, memory errors (e.g. double-free error) and assertion violations.


Given a C/C++ program as inputs (that uses C/C++11 atomics and/or concurrency primitives from the pthread library), it reports any data races, assertion violations, or other errors encountered. The verification can be performed with respect to the RC11 memory model (default), or other models such as IMM and LKMM.


C C++ LLVM Model checking


Related papers

GenMC: A Model Checker for Weak Memory Models (CAV '21)

Last publication date

15 July 2021

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.