The C Bounded Model Checker (and how to succeed at SV-COMP)

Michael Tautschnig

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.

Background Reading:

Speaker Bio: Michael Tautschnig is a Research Scientist at Amazon Web Services and lecturer at Queen Mary University of London. He obtained his PhD from Vienna University of Technology developing an efficient, systematic, and automatic test input generation technique for C programs. Prior to his appointment as lecturer he was a post-doctoral research assistant at the University of Oxford. A year ago he also joined Byron Cook's group at Amazon Web Services to apply his research at scale.
His current and recent research focusses automating verification for real-world software at large scale, and efficient software verification techniques for concurrent, shared-memory systems with relaxed memory models.