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

Application domain/field

• Bounded model checking
• Model checking
• Concurrency

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