PV1 Cerberus-BMCchecks a C program against a predefined concurrency model

Application domain/field

Type of tool

Model checker

Expected input

C program


.c file


Tool to explore allowed behaviours of C test programs that takes into account the concurrency memory model, the memory object model and the thread-local sequential semantics. Loop unwinding Uses Z3
C Concurrency Model checking


Related papers

Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C

Last publication date

12 July 2019

ProVerB specific

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