---
title: "Symbolic execution"
subject: "Software Engineering"
chapter: 7
key: "semester_5/software_engineering:symbolic-execution"
source: https://www.bctengineer.com/q/semester_5/software_engineering/symbolic-execution
site: BCT Engineering
---

# Symbolic execution

Software Engineering · Chapter 7: Verification and validation

- Asked in: 2067 Ashadh (old course), 4 marks
- Video: [Introducing Symbolic Execution](https://www.youtube.com/watch?v=cjNTsCqbf5k) — Software Security
- Answer checked by Claude Opus 5.5 (high effort) on 2026-10-14
- Page: https://www.bctengineer.com/q/semester_5/software_engineering/symbolic-execution
- Whole chapter: https://www.bctengineer.com/md/semester_5/software_engineering/chapter-7

## Question

Define symbolic execution in the context of software engineering.

## Short answer

Symbolic execution is a static verification technique where a program is executed with symbolic inputs instead of concrete values. Variables hold algebraic expressions, and at each branch a path condition is recorded. It is used to generate test inputs, find error paths, and verify path correctness, but suffers from path explosion.

## Answer

**Symbolic execution** is a static verification technique in which a program is "executed" with **symbols** (such as X and Y) as inputs instead of actual values. Variables then hold algebraic expressions of the inputs, and at each branch the condition on the inputs is recorded as a **path condition**. The result for each path is the output expressed as a formula in terms of the inputs, together with the condition under which that path is taken.

#### How it works
1. Assign symbolic values to all inputs.
2. Execute statements, updating variables with symbolic expressions.
3. At each `if` or loop, split into two paths and add the condition (or its negation) to the path condition.
4. A path whose condition cannot be satisfied is infeasible and is dropped.
5. For each feasible path, solve the path condition to get concrete test inputs, or check that the output meets the specification.

#### Example
```text
int f(int x, int y) {
    int z = 2 * y;
    if (z == x)
        if (x > y + 10)
            error();
    return 0;
}
```
With x = X, y = Y, we get z = 2Y:

| Path | Path condition | Result |
|---|---|---|
| 1 | 2Y != X | returns 0 |
| 2 | 2Y == X and X <= Y + 10 | returns 0 |
| 3 | 2Y == X and X > Y + 10 | error() |

Solving path 3 gives Y > 10, for example Y = 11, X = 22. A random test would rarely find these values, but symbolic execution finds them directly.

#### Uses and limits
- **Uses:** verifying that each path meets its specification, automatic test case generation, finding unreachable code and error paths. Tools such as KLEE and Java PathFinder use it.
- **Limits:** the number of paths grows very fast with loops and branches (**path explosion**); loops with unknown bounds, pointers and complex arithmetic make expressions hard to solve.

## Check yourself

The answer's key points as multiple-choice questions, with the correct option and why.

1. What does symbolic execution use as program inputs?
   A. Random numbers
   B. Symbols such as X and Y, so variables hold algebraic expressions
   C. Only the boundary values
   D. Values typed by the user at run time
   Answer: B. Inputs are symbols, so variables hold expressions of the inputs and each path gives a formula for the output. (Key point: Definition)

2. What is recorded at each branch during symbolic execution?
   A. The execution time
   B. The condition (or its negation) on the inputs, forming the path condition
   C. The memory address
   D. The number of lines executed
   Answer: B. At each if or loop the execution splits, adding the branch condition or its negation to the path condition. (Key point: Path condition)

3. For f with z = 2*y, and error() called when z == x and x > y + 10, what inputs reach error()?
   A. 2Y == X and Y > 10, e.g. X = 22, Y = 11
   B. 2Y != X
   C. 2Y == X and Y < 10
   D. X = Y
   Answer: A. With X = 2Y, the condition X > Y + 10 becomes 2Y > Y + 10, so Y > 10. Y = 11 gives X = 22. (Key point: Worked example)

4. What is the main limitation of symbolic execution?
   A. It needs the program to run on real hardware
   B. Path explosion with loops and branches
   C. It cannot generate test cases
   D. It only works on programs without conditions
   Answer: B. The number of paths grows very fast with loops and branches, and unbounded loops, pointers and complex arithmetic are hard to solve. (Key point: Limits)

## Related in Software Engineering

- [Short note: component-based software engineering](https://www.bctengineer.com/question.md?key=semester_5%2Fsoftware_engineering%3Acbse-note) — Software Engineering, chapter 6
- [Objectives of FTR; cleanroom software engineering](https://www.bctengineer.com/question.md?key=semester_5%2Fsoftware_engineering%3Aftr-cleanroom) — Software Engineering, chapter 9
- [Software errors and their impact on cost](https://www.bctengineer.com/question.md?key=semester_5%2Fsoftware_engineering%3Asoftware-errors-impact) — Software Engineering, chapter 7, asked 2×
- [Software reliability and reliability models](https://www.bctengineer.com/question.md?key=semester_5%2Fsoftware_engineering%3Areliability-models) — Software Engineering, chapter 9, asked 2×
- [Software crisis](https://www.bctengineer.com/question.md?key=semester_5%2Fsoftware_engineering%3Asoftware-crisis) — Software Engineering, chapter 1
- [Short note: software safety](https://www.bctengineer.com/question.md?key=semester_5%2Fsoftware_engineering%3Asoftware-safety) — Software Engineering, chapter 7

## Related in other subjects

- [Process vs thread; context switching](https://www.bctengineer.com/question.md?key=semester_6%2Foperating_system%3Athread-context-switching) — Operating System, chapter 2
- [Why estimate before execution (water supply)](https://www.bctengineer.com/question.md?key=semester_7%2Festimating_and_costing%3Aestimating-why-before-execution) — Estimating and Costing, chapter 1
- [Short note: Planning software, MS Project](https://www.bctengineer.com/question.md?key=semester_7%2Fproject_engineering%3Aplanning-software-ms-project-note) — Project Engineering, chapter 3, asked 2×
- [Software used for FEM and FDM](https://www.bctengineer.com/question.md?key=semester_8%2Fcomputational_techniques_in_civil_engineering%3Asoftware-fem-fdm) — Computational Techniques in Civil Engineering, chapter 1