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

Application domain/field

• Model checking
• Bounded model checking

Type of tool

Model checker

Expected input

• Program
• Optionally: Loop bound

Format:

• Program: C or C++ program
• Loop bound: Passed as an option when executing cbmc

Expected output

• Error/warning when a property is violated.
• Optionally: If an assertion is violated, CBMC can give a counterexample trace where the assertion is violated. This trace can either be printed or output in an XML file.
• Optionally: a list the properties that it checks.
• Optionally: the verification conditions that are generated.

Internals

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.

Comments

It is part of CProver