The basic idea is to make variables hold symbolic expressions instead of concrete ones. So executing a statement like "a=b*c" doesn't actually execute multiplication, it just notes that now "a" holds the value "Multiply(b,c)". When you get to a point where there's a test on the value of "a", you run a constraint checker (an automated prover) to decide if the test could be true or not, and if true with what set of variables. So you could find, for example, an integer overrun by checking whether "a" is always positive; and if not it'll give you values of "b" and "c" that demonstrate it's not. (Or, more likely, the values of the inputs that led to "b" and "c" having the values which led to integer overflow.)
This seems like a very strong tool for systems programming. I've been thinking of playing around with the idea of a language whose compiler produces correctness proofs along with generated code. But this will work on (most) C code--- they ran it on the GNU Coreutils collection. The project seems to be reasonably active (the original paper was 2008).