Symbolic Execution

Diving into Symbolic Execution

Instead of supplying the normal inputs to a program one supplies symbols representing arbitrary values

The execution proceeds as in a normal execution except that values may be symbolic formulas over the input symbols.

large-scale production of reliable programs

Instead of executing a program on a set of sample inputs, a program is “symbolically” executed for a set of classes of inputs.

If the control flow of the program is completely independent of the input variables, a single symbolic execution will suffice to check all possible executions of the programs.

What is Symbolic Execution?

Symbolic execution allows for the exploration of a large class of program executions using a single symbolic execution. This can be advantageous in program testing and debugging. It has applications in test case generation and program optimization.

Effigy is an example of a symbolic execution system that provides features for program testing, debugging, and verification. It allows for interactive exploration of the execution tree and includes facilities for managing and proving things about symbolic expressions.

Symbolic execution can be used to generate test data and symbolically execute programs, providing a way to systematically explore different program paths. It can also be used for program improvement and optimization.

Overall, symbolic execution offers a powerful approach to program analysis and provides valuable insights into the general notion of symbolic execution and its various applications.

KLEE

Symbolic execution is a technique used in program analysis, testing, and optimization. It involves executing a program using symbols to represent inputs instead of concrete values. When program execution branches based on a symbolic value, the system (conceptually) follows both branches, on each path maintaining a set of constraints called the path condition which must hold on execution of that path. When a path terminates or hits a bug, a test case can be generated by solving the current path condition for concrete values.

Practical Issues

Many of the troublesome issues arising in program proving systems also occur in symbolic execution.

Finding a practical way to deal with variable storage-referencing
The array notation references a different particular element of the array A depending on the value of I
Conflict between discrete aspects of computer arithmetric
The continuous nature of real numbers with infinite precision
A gap between the truth of a predicate and the ability of an automatic theorem prover to establish its truth
Solutions
An obvious way to enhance symbolic execution to provide correctness proof in all cases is to consider some form of induction over the infinite parts of the execution tree.