Angr – User-friendly binary analysis platform
github.com
github.com
Angr is also the open-source part of the Shellphish/UCSB contestant (Mechanical Phish) that competed in the DARPA CGC [2].
[1] - https://en.wikipedia.org/wiki/Concolic_testing
[2] - https://en.wikipedia.org/wiki/2016_Cyber_Grand_Challenge
It's not the only open-source part: https://github.com/mechaphish
1. BAP (OCaml) - https://github.com/BinaryAnalysisPlatform/bap
2. BinCAT (OCaml) - https://github.com/airbus-seclab/bincat
3. radare2 (C) + radeco (Rust)(WIP) - https://github.com/radare/radare2 + https://github.com/radare/radeco-lib
4. Falcon (Rust) (WIP) - https://github.com/falconre/falcon
And a bunch of others, less common or less featureful.
You can also use CBMC to solve the usual state reverse engineering problems, like coverage analysis, finding input for output, hash collisions, ...