TL;DR
This survey reviews the development, main ideas, challenges, and solutions of symbolic execution, a technique for systematically exploring program execution paths to improve software testing and security analysis.
Contribution
It provides a comprehensive overview of symbolic execution techniques, distilling four decades of research and practical tool development for a broad audience.
Findings
Symbolic execution enables systematic exploration of program paths.
Constraint solvers are essential for constructing concrete inputs.
Major breakthroughs have been achieved in software reliability applications.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
