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,