SE547: CBMC: Summary [17/19]

CBMC is a C Bounded Model Checker. It can help with bug hunting by exhaustively searching for failed assertions.

CBMC translates C down to predicate logic, and throws the problem to a SAT-solver.

The resulting system does not catch every bug, but it catches quite a lot!