Or angr (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)
Or angr (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)
Or manticore (you'll need IDA Pro there ?) : https://blog.trailofbits.com/2017/04/27/manticore-symbolic-e...
There's a good survey there : 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.