Angr / z3 (Symbolic execution / SAT solver)
https://github.com/FSecureLABS/z3_and_angr_binary_analysis_workshop