Glossary
Symbolic Execution
A program analysis technique that executes code with symbolic (abstract) values instead of concrete inputs, exploring multiple paths simultaneously.
Symbolic execution is a program analysis technique that runs code using symbolic rather than concrete values — each unknown input is represented as a mathematical symbol. The engine tracks constraints on those symbols (e.g., "symbol X must be > 0 for this branch to be taken") and uses an SMT solver (like Z3) to find concrete inputs that satisfy any desired path condition. In reverse engineering, symbolic execution is used to automatically solve crackmes, bypass license checks, find bug-triggering inputs, and de-obfuscate code. Popular frameworks include angr (Python), Triton, and Manticore. It scales poorly on large binaries — a problem known as path explosion.