A Survey of Symbolic Execution Techniques
By Roberto Baldoni, Emilio Coppa, Daniele Cono D'Elia, Camil Demetrescu, Irene Finocchi. ACM Computing Surveys, 2016
801 citations recorded by the source corpus.
Many security and software testing applications require checking whether certain properties of a program hold for any possible usage scenario. For instance, a tool for identifying software vulnerabilities may need to rule out the existence of any backdoor to bypass a program’s authentication. One approach would be to test the program using different, possibly random inputs. As the backdoor may only be hit for very specific program workloads, automated exploration of the space of possible inputs is of the essence. Symbolic execution provides an elegant solution to the problem, by systematically exploring many possible execution paths at the same time without necessarily requiring concrete inputs. Rather than taking on fully specified input values, the technique abstractly represents them as symbols, resorting to constraint solvers to construct actual instances that would cause property violations. Symbolic execution has been incubated in dozens of tools developed over the past four decades, leading to major practical breakthroughs in a number of prominent software reliability applications. The goal of this survey is to provide an overview of the main ideas, challenges, and solutions developed in the area, distilling them for a broad audience.
Subfields: Software, Signal Processing
View Paper: https://www.semanticscholar.org/paper/1a6065f26e0b3407c0063ed76b847f9c3895275c
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Software
In Signal Processing
Citations in the corpus
- Survey on the Usage of Machine Learning Techniques for Malware Analysis (2017, background): “ [81, 82] and other operations aimed at supporting binary reverse engineering, such as function similarity identication [83], are still very active research directions. Symbolic execution techniques [84] are promising means to understand what execution paths trigger the launch of the malicious paylo”