PV3 CBMC: C Bounded Model Checkerverifies given/parameterised properties of C code

Application domain/field

Type of tool

Model checker

Expected input


Expected output


Loop unwinding Bounded model checking: check if a property holds for traces up to n steps (i.e. length of the trace). SAT solving It can verify array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions. Note that for some of these checks you need to pass specific options when executing cbmc.


It is part of CProver
C C++ Model checking


Related papers

Last publication date

18 July 2018

ProVerB specific

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