CBMC is a Bounded Model Checker for C and C++ programs.
It supports C89, C99, most of C11/C17 and most compiler extensions
provided by gcc, clang, and Visual Studio. A variant of CBMC that
analyses Java bytecode is available as JBMC.
[Set JBMC=ON to enable JBMC.]

CBMC verifies memory safety (which includes array bounds checks
and checks for the safe use of pointers), checks for exceptions,
checks for various variants of undefined behavior, and
user-specified assertions. Furthermore, it can check C and C++ for
I/O equivalence 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.

CBMC comes with a built-in solver for bit-vector formulas that is
based on MiniSat. As an alternative, CBMC has featured support for
external SMT solvers since version 3.3. The solvers we recommend
are (in no particular order) Boolector, CVC5 and Z3. Note that
these solvers need to be installed separately and have different
licensing conditions.
[This SlackBuild builds Cadical as the internal solver.]

If you need a Model Checker for Verilog or SMV files, consider
EBMC. For Java, use JBMC.

This research was sponsored by the Semiconductor Research
Corporation (SRC) under contract no. 99-TJ-684, the National
Science Foundation (NSF) under grant no. CCR-9803774, the Office
of Naval Research (ONR), the Naval Research Laboratory (NRL) under
contract no. N00014-01-1-0796, and by the Defense Advanced
Research Projects Agency, and the Army Research Office (ARO) under
contract no. DAAD19-01-1-0485, and the General Motors
Collaborative Research Lab at CMU. The views and conclusions
contained in this document are those of the author and should not
be interpreted as representing the official policies, either
expressed or implied, of SRC, NSF, ONR, NRL, DOD, ARO, or the U.S.
government.