Finding Software Bugs Using Symbolic Execution
The idea of dynamic symbolic execution is to execute a piece of software on any input. All possible execution paths are explored simultaneously without specifying concrete values. Consider the following example where the input x is unknown, i.e., symbolic: if (x < 0) { // ... } else if (x > 100) { // ... } else { assert("should not reach this!") } Symbolic execution runs this code on all three…