Package cbmc

Bounded Model Checker for ANSI-C and C++ programs

CBMC generates traces that demonstrate how an assertion can be violated, or
proves that the assertion cannot be violated within a given number of loop

Version: 5.95.1

General Commands

cbmc Bounded Model Checker for C/C++ and Java programs
crangler C source transformation
goto-analyzer Data-flow analysis for C programs and goto binaries
goto-cc C/C++ to goto compiler
goto-diff Syntactic diff of goto binaries
goto-gcc alias for goto-cc
goto-harness Generate environments for symbolic analysis
goto-instrument Perform analysis or instrumentation of goto binaries
goto-ld alias for goto-cc
goto-synthesizer Synthesize and apply loop contracts of goto binaries.
memory-analyzer Snapshot program state for symbolic analysis
symtab2gb Compile JSON symbol tables to a GOTO binary