In particular, one of the more important rules I made when using CBMC was to keep the search depth for each invocation as shallow as possible. If CBMC runs in less than five minutes, you're doing it right. If it takes more than that, then you're asking it to do too much.

This led to the creation of function contracts and shadow functions. When evaluating functions, we actually want any calls that it makes to go to shadow functions instead of real functions. When we write a function, we include a contract that includes anything it may return, any side-effects it may have, and any memory it may touch / allocate / initialize. We then write a twin function -- its shadow function -- that technically follows the same contract in the most simplified terms, randomly choosing whether to succeed or fail. From CBMC's perspective, it's equivalent enough for model checking. But, it removes additional stack depth or recursion.

A good example of this would be a shadow function for the POSIX read function. Its contract should verify that the descriptor it is passed is valid. It should also assert that the memory region it is passed is bounded by the size it is given. The shadow function picks a non-deterministic state based on how it should set errno and how it should return. This state follows the POSIX standard, but the underlying system calls don't matter. Likewise, depending on the return code, it should initialize a number of bytes in the read buffer with non-deterministic values.

I used this shadow read function to find a buffer overflow in networking code and also to find a DOS infinite loop error in a tagged binary file format reader we were using.

CBMC isn't perfect, but when coupled with a good linter and -Wall / -Werror / -Wpedantic, it is a very useful layer in a defense in depth strategy for safer software.

> CBMC isn't perfect, but when coupled with a good linter and -Wall / -Werror / -Wpedantic, it is a very useful layer in a defense in depth strategy for safer software.

I agree to a certain extent, but at what point are you putting in more effort than it would take to migrate to a stricter language that offers more safety by default?

I'm not aware of any language that can't be improved by this strategy. Amazon even added SMT solving tooling around Rust, because Rust's built-in safety guarantees aren't enough.

I'd say that the added effort is minimal. The compiler spits out more errors. We think a little more carefully about how we write functions so CBMC doesn't complain. There are no silver bullets.

>Satisfiability Modulo theories (SMT) is an area of automated deduction that studies methods for checking the satisfiability of first-order formulas with respect to some logical theory T of interest. It differs from general automated deduction in that the background theory T need not be finitely or even first-order axiomatizable, and specialized inference methods are used for each theory. By being theory-specific and restricting their language to certain classes of formulas (such as, typically but not exclusively, quantifier-free formulas), these specialized methods can be implemented in solvers that are more efficient in practice than general-purpose theorem provers.

>While SMT techniques have been traditionally used to support deductive software verification, they are now finding applications in other areas of computer science such as, for instance, planning, model checking and automated test generation. Typical theories of interest in these applications include formalizations of arithmetic, arrays, bit vectors, algebraic datatypes, equality with uninterpreted functions, and various combinations of these.

http://smtlib.cs.uiowa.edu/about.shtml