📦 cbmc

C

• cbmc(1)Bounded Model Checker for C/C++ and Java programs✨
• crangler(1)C source transformation✨

G

• goto-analyzer(1)Data-flow analysis for C programs and goto binaries✨
• goto-cc(1)C/C++ to goto compiler✨
• goto-diff(1)Syntactic diff of goto binaries✨
• goto-gcc(1)C/C++ to goto compiler✨
• goto-harness(1)Generate environments for symbolic analysis✨
• goto-inspect(2)Inspect goto-binaries.✨
• goto-instrument(1)Perform analysis or instrumentation of goto binaries✨
• goto-ld(1)C/C++ to goto compiler✨
• goto-synthesizer(1)Synthesize and apply loop contracts of goto binaries.✨

J

• janalyzer(1)Data-flow analysis for Java bytecode✨
• jbmc(1)Bounded model checking for Java bytecode✨
• jdiff(1)Syntactic diff of goto programs obtained from Java bytecode✨

M

• memory-analyzer(1)Snapshot program state for symbolic analysis✨

S

• symtab2gb(1)Compile JSON symbol tables to a GOTO binary✨