Or cbmc (some interesting papers : http://www.cprover.org/cbmc/applications/ http://www.cprover.org/cbmc/applications/), they're on GitHub : https://github.com/

Or cbmc (some interesting papers : http://www.cprover.org/cbmc/applications/ http://www.cprover.org/cbmc/applications/), they're on GitHub : https://github.com/diffblue/cbmc https://github.com/diffblue/cbmc), seems to also handle java, not sure... Or angr (http://angr.io http://angr.io) which works on binaries and is in python and is loads of fun to use... On small codebases ? Still some people have used it in combination with AFL to help the fuzzer when it's stuck ('driller' : https://github.com/shellphish/driller https://github.com/shellphish/driller) Or manticore (you'll need IDA Pro there ?) : https://blog.trailofbits.com/2017/04/27/manticore-symbolic-execution-for-humans/ https://blog.trailofbits.com/2017/04/27/manticore-symbolic-e... There's a good survey there : https://arxiv.org/abs/1610.00502 https://arxiv.org/abs/1610.00502 (no cbmc though). But nickpsecurity is right, Klee seems to be the place where most of the interesting stuff seems to be happening right now. The recent improvements in SMT/SAT solvers bring back lots of techs that were thought impractical (formal proof, symbolic execution...) a while back.