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

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/ https://github.com/trailofbits/deepstate/