Triton

It provides internal components that allow you to build your program analysis tools, automate reverse engineering, perform software verification or just emulate code.
- Dynamic symbolic execution
- Dynamic taint analysis
- AST representation of the x86, x86-64, ARM32 and AArch64 ISA semantic
- Expressions synthesis
- SMT simplification passes
- Lifting to LLVM as well as Z3 and back
- SMT solver interface to Z3 and Bitwuzla
- C++ and Python API