CBMC vs SPIN

CBMC is a bounded model checker for C and C++ programs. It explores execution paths to check assertions, including array bounds, pointer safety, exceptions, and some undefined behavior such as signed integer overflow. Its analysis unwinds loops before sending the resulting equation to a decision procedure, and inputs may need a bounded size. The repository lists C89, C99, most of C11, C17, C23, GCC and Visual Studio extensions, and SystemC through Scoot; the listed input languages also include Java bytecode. CBMC supports contracts and can produce counterexamples. Its incremental SMT2 backend works with SMT-LIB 2.6-compliant solvers, with Z3 and CVC5 as examples. Distribution options include Homebrew instructions for macOS, Ubuntu DEB packages, Windows MSI installers, and Docker images. goto-cc can replace gcc or cl.exe in Makefiles to collect project models. The guide discusses routine development and continuous integration use. CBMC is free under the 4-clause BSD license.

SPIN is a free, self-hosted model-checking tool for analyzing the logical consistency of asynchronous systems, including distributed software and communication protocols. Systems are specified in Promela, which represents asynchronous processes, nondeterministic choices, loops, and local or global variables. Models can state correctness requirements, including linear temporal logic. SPIN supports interactive, guided, and random simulations of execution. For verification, it generates a C program for exhaustive or approximate checking of those requirements. Its product description lists detection of deadlocks, race conditions, incomplete specifications, and unjustified assumptions about process speeds. Partial order reduction optimizes verification runs, while the site provides guidance for multicore depth-first and breadth-first algorithms and swarm methods for large state spaces. SPIN runs on Linux, macOS, and Windows, as well as other listed systems. From version 6.4.5, its code, sources, and executables use the BSD 3-Clause license. Verification requires a working C compiler and preprocessor. The optional iSpin graphical interface is written in Tcl/Tk and requires Tcl/Tk.