What is Symbolic Execution?
June 20, 2019
Summary
A way to analyze which inputs cause parts of a program to execute. A special interpreter assumes symbols instead of static inputs like an abstract interpretation of the program, and determines a set of expressions which lead to particular code paths to be executed, and a set of constraints for each possible outcomes of the code branches.
A good reference to understand Symbolic Execution is this.
Limitations
Does not work particularly well with large programs as number of expressions and constraints increase exponentially with increased code paths.
Does not work when program depends on components which depend on the environment. Eg if SYSCALLS/UPCALLS or interrupts are involved, eg opening a file in a program.