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

Application domain/field

Type of tool

Model checker

Expected input

C program

Format:

.c file

Internals

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

Links

Related papers

https://doi.org/10.1007/978-3-030-25540-4_22

Last publication date

12 July 2019

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.