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.