What I'm personally hinting at is symbolic/concolic execution. Essentially, each variable has a set of constraints associated with it - initially left blank for an input variable, for example. Then, the program can be executed, with assignments producing new constraints and replacing old ones. At each point in control flow, the executor chooses a path, and adds new constraints. When a dangerous statement (assertion, pointer dereference etc) is reached, the constraints can be solved by z3 or some other SMT solver, and if it can find a satisfying result you automatically have a test case that will produce erroneous or undefined behaviour.

It works quite well for short programs, actually - the KLEE people (or maybe it was DART) found bugs in busybox, GNU Coreutils etc.

The current approach is to instead of traversing your control flow tree explicitly (which means you're doing a tree search over a potentially infinite tree), converting the program such that it produces a logical statement that can be solved by an SMT solver, that is satisfiable iff there is an input that leads to a bug within that bounded number of loop unwindings.

With fun C++ metaprogramming, you can actually get this to happen natively (i.e. the parts that aren't reliant on input get run natively) which leads to a massive speedup o

I don't believe it to be model checking, although it might use model checking techniques. I could be wrong, I'm only familiar with a few aspects.