Or cbmc (some interesting papers : http://www.cprover.org/cbmc/applications/), they're on GitHub : https://github.com/diffblue/cbmc), seems to also handle java, not sure...

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.

I recommend people look through their whole publication list here:

http://klee.github.io/publications/

That group does some amazing work bridging neat theories and putting things into practice. I wish more researchers would build on KLEE to see just how much more it could accomplish. That is, on top of more developers using tools like it.