blob: 2004194d7c43115e7fe64439f0d9e785216a5534 (
plain) (
blame)
1
2
3
4
5
6
7
|
CBMC is a Bounded Model Checker for C and C++ programs.
It supports C89, C99, most of C11 and most compiler extensions provided by gcc
and Visual Studio. It allows verifying array bounds (buffer overflows), pointer
safety, exceptions and user-specified assertions. Furthermore, it can check C
and C++ for consistency with other languages, such as Verilog.
The verification is performed by unwinding the loops in the program and passing
the resulting equation to a decision procedure.
|
