Finding Software Bugs Using Symbolic Execution

This article is interesting in context. You're trying to select tests to run. Instead of using educated guesses about parameters (combinatorial interaction designs), you're going to look at the system under test. You could generate lots of tests and see what worked by looking at coverage of those tests (line coverage or mutation coverage). Instead, you'll analyze the code with symbolic execution and make choices. Klee seems like best-in-class for symbolic execution. A more popular alternative these days is concolic execution, which combines concrete execution with symbolic constraint solving. That's in Pex and Intellisense.

Looking at some of your SMT-based projects, I'd love to compare your SMT solver notes with my mine from working on https://github.com/pschanely/CrossHair

Sadly, there aren't a lot of resources on how to use SMT solvers well.

This is "simple" in theory, but actually very difficult to implement in the general case. Automated testing has been more or less an open area of research for decades. It's "easy" to see how to trip branches in a case where an int has to be above 20 or whatever, but in reality, when dealing with ad-hoc (& often intractable) memory mappings, fancy pointer arithmetic, or more interesting paradigms (e.g. recursive calls that may break somewhere down the line), this becomes several orders of magnitudes harder to do.

You might be interested in GUEB[1] as well.

It's a PhD project that implements symbolic execution. It has been able to find real-life vulerabilities.

[1] https://github.com/montyly/gueb

But covering all branches does not mean that the program doesn’t have any bugs. Things like condition coverage and modified condition / decision coverage exist because of this. You need to ensure that all possible inputs are handled correctly by the code, which is a much harder problem than traversing all branches.

I think I understand the concept. But if you trip an assertion like in the example code, that means there was a bug prior to the function call... (and the program would crash with a dump and stack). I however see no point in unit testing that function (unless its more complicated then the example code)