KLEE: A symbolic virtual machine built on top of LLVM

This is the KLEE project mentioned in "The PhD Grind" book [0], which was also on HN recently. I recommend reading it for a behind-the-scenes look at the effort required to complete a PhD in CS.

[0] http://www.pgbovine.net/PhD-memoir.htm

I just played with this just a few days ago to solve some crackme challenges. It is pretty cool: decompile the binary, use KLEE to symbolize inputs, ..., profit.

There is also DeepState[0], which is quite similar (provides a higher abstraction) for test harnesses

[0]: https://github.com/trailofbits/deepstate/

This looks incredible. Will definitely be playing with this in the coming days.

If you think that's cool, you might be interested in S²E: http://s2e.systems/