Approach #13: Symbolic Execution - Explore All Paths #17
Description
Symbolic Execution: Explore ALL Execution Paths
Use symbolic (not concrete) values. Find inputs that trigger behaviors.
Process
Input: a = α (symbolic), b = β (symbolic)
Path 1: β == 0
Constraint: β == 0
Example: b = 0
Result: Division by zero error
Path 2: β != 0
Constraint: β != 0
Example: b = 1
Result: returns α ÷ β
Finds
- All possible execution paths
- Inputs that trigger each path
- Invariant violations on any path
Strengths
✅ Exhaustive path coverage
✅ Finds corner cases
✅ Security vulnerabilities
Weaknesses
❌ Path explosion (exponential growth)
❌ Limited Dart tooling