CBMC About CBMC CBMC is a Bounded Model Checker for C and C++ programs. It sup­ports C89, C99, most of C11/C17 and most compi­ler exten­sions pro­vided by gcc, clang, and Visual Studio. A variant of CBMC that analyses Java bytecode is available as JBMC. CBMC verifies memory safety (which includes array bounds checks and checks for the safe use of pointers), checks for ex­cep­tions, checks for various variants of undefined behavior, and user-specified as­ser­tions. Further­more, it can check C ...