Abstract: "Many security and software testing applications require checking whether certain properties of a programhold for any possible usage scenario. For instance, a tool for identifying software vulnerabilities may need torule out the existence of any backdoor to bypass a program’s authentication. One approach would be to test theprogram using different, possibly random inputs. As the backdoor may only be hit for very specific programworkloads, automated exploration of the space of possible inputs is of the essence. Symbolic execution providesan elegant solution to the problem, by systematically exploring many possible execution paths at the sametime without necessarily requiring concrete inputs. Rather than taking on fully specified input values, thetechnique abstractly represents them as symbols, resorting to constraint solvers to construct actual instancesthat would cause property violations. Symbolic execution has been incubated in dozens of tools developed overthe last four decades, leading to major practical breakthroughs in a number of prominent software reliabilityapplications. The goal of this survey is to provide an overview of the main ideas, challenges, and solutionsdeveloped in the area, distilling them for a broad audience."