Symbolic Execution (SE) enables a precise, deep program exploration by executing programs with symbolic inputs. Traditionally, the SE community is divided into the rarely interacting sub-communities of bug finders and program provers. This has led to independent developments of related techniques, and biased surveys and foundational papers. As both communities focused on their specific problems, the foundations of SE as a whole were not sufficiently studied. We attempt an unbiased account on the foundations, central techniques, current applications, and future perspectives of SE. We first describe essential design elements of symbolic executors, supported by implementations in a digital companion volume. We recap a semantic framework, and derive from it a—yet unpublished—automatic testing approach for SE engines. Second, we introduce SE techniques ranging from concolic execution over compositional SE to state merging. Third, we discuss applications of SE, including test generation, program verification, and symbolic debugging. Finally, we address the future. Google’s OSS-Fuzz project routinely detects thousands of bugs in hundreds of major open source projects. What can symbolic execution contribute to future software verification in the presence of such competition?
2022
2024-09-20