Symbolic Execution for Software Testing: Three Decades Later.

The article presents an overview of modern and classical symbolic execution techniques which are used in software testing to explore program paths and to find errors in complex software applications. The article notes the input values for symbolic execution are symbolic values, the values of a computer program's variables are symbolic expressions, and the computed output values represent a function of the input symbolic values. The challenges of symbolic execution such as path explosion, constraint solving, and memory modeling are also mentioned. Topics include execution-generated testing (EGT) and directed automated random testing (DART).