Symbolic execution

Symbolic execution is a way of analyzing a program to work out which inputs cause each part of it to run. Instead of reading real input values, an interpreter follows the program with symbolic placeholders standing in for the inputs. It ends up with expressions over those symbols for variables and, for each conditional branch, a constraint that describes when each outcome happens. At a branch the analysis forks into two paths, each carrying its own copy of the program state and its own path constraint. When a path ends, solving its accumulated constraints yields concrete inputs, which can serve as test cases that help developers reproduce bugs. The method reasons path by path rather than input by input, but it struggles with path explosion in large programs, with aliasing of memory, with arrays and with interactions with the environment such as system calls. Tools such as KLEE take the approach of modeling the environment. The concept was introduced academically in the 1970s through systems named Select, EFFIGY, DISSECT and Clarke system.