Chapter Six - Symbolic Execution and Recent Applications to Worst-Case Execution, Load Testing, and Security Analysis.

Symbolic execution is a systematic program analysis technique which executes programs on symbolic inputs, representing multiple concrete inputs, and represents the program behavior using mathematical constraints over the symbolic inputs. Solving the constraints with off-the-shelf solvers yields inputs that exercise different program paths. Typical applications of the technique include test input generation and error detection. In this chapter we review symbolic execution and associated tools, and describe some of the main challenges in applying symbolic execution in practice: handling of programs with complex inputs, coping with path explosion, and ameliorating the cost of constraint solving. We also survey promising applications of the technique that go beyond checking functional properties of programs. These include finding worst-case execution time in programs, load testing and security analysis, via combinations of symbolic execution with fuzzing.