CBMC implements bit-precise bounded model checking for C programs and has been
developed and maintained for more than ten years. Only recently support for
efficiently checking concurrent programs, including support for weak memory
models, has been added. CBMC verifies the absence of violated assertions under
a given loop unwinding bound by reducing the problem to a Boolean formula. The
formula is passed to a SAT solver, which returns a model if and only if the
property is violated.
CBMC's support ranges from basic integer programs to IEEE 754 floating point and
concurrent programs. The tool chain around CBMC enables applications to full
software systems, such as analysing a SAT solver and more recently has been
applied across the entire Debian/GNU Linux distribution.
At the 2017 TACAS Software Verification Competition (SV-COMP'17) CBMC has won
the "Falsification" category, making CBMC the most efficient and precise bug
hunting tool. The results will be discussed in detail in Uppsala in April during
ETAPS, which has previously been hosted at QMUL by the Theory group in 2015.
Cornwallis South West,
University of Kent,