A program branches on the condition (x > 5). Under symbolic execution with x as a symbolic variable, what happens at this branch point?
AThe symbolic executor picks a random value for x and follows one path
BExecution forks into two paths: one with the constraint x > 5 added to the path condition, and one with x <= 5 added. Both paths are explored independently
CThe branch is skipped and both paths are merged
DThe symbolic executor evaluates x > 5 to 'unknown' and halts
Forking at branches is the core mechanism of symbolic execution. Each fork creates an independent execution path with its own path constraint. The path exploring the then-branch knows x > 5; the path exploring the else-branch knows x <= 5. When a path reaches a target (assertion violation, error, or exit), the SMT solver finds a concrete input satisfying the accumulated path constraints, producing a test case that exercises that exact path.
Question 2 Short Answer
The path explosion problem in symbolic execution — the number of paths growing exponentially with the number of branches — is analogous to which problem in model checking?
Think about your answer, then reveal below.
Model answer: The state explosion problem. In model checking, the number of states grows exponentially with the number of concurrent components. In symbolic execution, the number of paths grows exponentially with the number of branch points (each branch doubles the paths). Both require techniques to manage exponential blowup: model checking uses symbolic methods (BDDs) and abstraction (CEGAR); symbolic execution uses heuristic path selection, path merging, and concolic execution to focus on interesting paths.
The duality is striking. Model checking explores states; symbolic execution explores paths. Both face exponential blowup. Both are fully automatic within their scope but need engineering to scale. The parallel motivates hybrid approaches: bounded model checking (which unrolls execution for a fixed number of steps) is essentially symbolic execution with a depth bound, and directed symbolic execution uses model-checking ideas to prune redundant paths.
Question 3 Short Answer
Concolic (concrete + symbolic) execution runs the program with both concrete and symbolic inputs simultaneously. What advantage does this provide over pure symbolic execution?
Think about your answer, then reveal below.
Model answer: Concolic execution uses concrete execution to drive the program forward through code that is difficult for pure symbolic execution (native library calls, complex pointer arithmetic, system calls) while maintaining symbolic constraints alongside. When the program reaches a branch, the symbolic constraints are negated to generate inputs for alternative paths. This avoids getting stuck on operations that cannot be symbolically modeled, at the cost of potentially missing some paths that pure symbolic execution would explore.
Pure symbolic execution must model every operation symbolically, which is impractical for system calls, native libraries, or floating-point arithmetic. Concolic execution sidesteps this by executing concretely (always making progress) while tracking symbolic constraints for the operations it CAN model. Tools like SAGE (Microsoft) and KLEE use variants of this approach to test real-world software including operating systems and device drivers.