[jlouis]

Yep, but in the dual, they have the same goal: produce interesting inputs to the program which might exhibit trouble.

This is why you can use one of the approaches to help the other side of the approach.

The 3rd solution is concolic testing: use an SMT/SAT solver to flip branches. The path down to the branch imposes a formula. By inverting the formula, we can pick a certain branch path. Now you ask the SMT solver to check there there's no way to go down that branch. If it finds satisfiability, you have a counterexample and can explore that path.

[UncleMeat]

Being thematically similar is not that interesting, if one works better than the others.

Coverage guided fuzzing is eating symbolic execution and concolic testing for breakfast. It isn't even close. As much as I love these more principled approaches, the strategy of throwing bits at programs and applying careful coverage metrics is just way more effective, even for cases that seem to be hand picked for SMT-based approaches to win.