CBMC vs UPPAAL

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.

UPPAAL is an integrated environment for modeling, simulating, and verifying real-time systems as networks of timed automata. Its language supports clock and data variables, including bounded integers and arrays. The model checker uses symbolic state-space exploration for invariant and reachability properties and can produce diagnostic traces. Statistical Model Checking estimates probabilities, compares a probability with a value, or compares two probabilities. UPPAAL Stratego supports generating, optimizing, comparing, and exploring strategies for stochastic priced timed games. Related tools include CORA, TRON, TIGA, ECDAR, and COSHY for cost-optimal analysis, testing, timed games, refinement, and hybrid-system control. Typical applications include real-time controllers and timing-critical communication protocols. Desktop packages support Windows, macOS, and Linux, including macOS x86_64 and Aarch64. The graphical interface needs Java 17 or later; verifyta runs without Java. Academic users register for a free license key, retrieved over the internet. Commercial and other non-academic use requires a separate license.