This talk provides a foundational introduction to symbolic execution. Symbolic execution is an automated software testing technique that enumerates all reachable execution paths through a software under test. An execution path is a sequence of Boolean values specifying which branch was taken, for every branch point in the tested software. As program execution diverts at branch points, reasoning about execution paths is vital for software testing.

To enumerate execution paths, symbolic execution formally reasons about the satisfiability of branch conditions. Therefore, in contrast to other automated testing techniques (e.g., fuzzing), it takes the program structure into account and thus goes beyond bug finding, enabling us to prove properties about the tested code. That is, show that they hold on all reachable execution paths. The presentation will explain how symbolic execution works under the hood and illustrate its outlined capabilities using a practical example.