Symbolic execution is a well-known program analysis technique that executes a program on symbolic inputs which represent all possible concrete program inputs. It systematically explores the program behaviors, while computing the values of conditions and variables in the program as constraints and expressions over the symbolic inputs. Solving the symbolic constraints yields test inputs that guarantee high coverage of the program. Symbolic execution has become very popular in recent years, due to both algorithmic advances and availability of computational power and efficient decision procedures. We review different flavors of symbolic execution, ranging from generalized symbolic execution to dynamic symbolic execution or concolic testing.

We identify challenges to symbolic execution such as dealing with looping constructs, multithreading, recursive data structures and complex mathematical constraints, as well as scalability issues due to the large number of program paths that are executed. We discuss techniques and tools that address these challenges and their application to software testing. We will also review other applications, such as security, robustness, reliability, load testing, invariant generation or program repair. We illustrate symbolic execution and its applications using the Symbolic PathFinder open-source tool available from: http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc.