There's whitebox fuzzing that's starting to become a thing, when your fuzzer gets stuck you give the non-giving corpus to an SMT solver and it'll try to see if there exists an input that could uncover a new path. I'm really excited about these but haven't really followed the advances.