# A Survey of Symbolic Execution Techniques

arXiv: https://arxiv.org/abs/1610.00502 · HTML: https://mlsanity.com/paper/1610.00502/

## Key facts

- Cited by 36 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 3 Oct 2016.

## Built on by (most cited first, 30 of 36)

- [CyberGym: Evaluating AI Agents' Real-World Cybersecurity Capabilities at Scale](https://mlsanity.com/paper/2506.02548/) (2025)
- [Code-Aware Prompting: A study of Coverage Guided Test Generation in Regression Setting using LLM](https://mlsanity.com/paper/2402.00097/) (2024)
- [SkillNet: Create, Evaluate, and Connect AI Skills](https://mlsanity.com/paper/2603.04448/) (2026)
- [CAT-LM: Training Language Models on Aligned Code And Tests](https://mlsanity.com/paper/2310.01602/) (2023)
- [A Quantitative Geometric Approach to Neural-Network Smoothness](https://mlsanity.com/paper/2203.01212/) (2022)
- [LLM-Powered Test Case Generation for Detecting Bugs in Plausible Programs](https://mlsanity.com/paper/2404.10304/) (2024)
- [Binary Code Summarization: Benchmarking ChatGPT/GPT-4 and Other Large Language Models](https://mlsanity.com/paper/2312.09601/) (2023)
- [Toward Trustworthy Neural Program Synthesis](https://mlsanity.com/paper/2210.00848/) (2022)
- [A Contemporary Survey of Large Language Model Assisted Program Analysis](https://mlsanity.com/paper/2502.18474/) (2025)
- [Safe Neurosymbolic Learning with Differentiable Symbolic Execution](https://mlsanity.com/paper/2203.07671/) (2022)
- [SACTOR: LLM-Driven Correct and Idiomatic C to Rust Translation with Static Analysis and FFI-Based Verification](https://mlsanity.com/paper/2503.12511/) (2025)
- [TestForge: Feedback-Driven, Agentic Test Suite Generation](https://mlsanity.com/paper/2503.14713/) (2025)
- [When Less is Enough: Positive and Unlabeled Learning Model for Vulnerability Detection](https://mlsanity.com/paper/2308.10523/) (2023)
- [Automating the Correctness Assessment of AI-generated Code for Security Contexts](https://mlsanity.com/paper/2310.18834/) (2023)
- [Generating executable oracles to check conformance of client code to requirements of JDK Javadocs using LLMs](https://mlsanity.com/paper/2411.01789/) (2024)
- [MANDO: Multi-Level Heterogeneous Graph Embeddings for Fine-Grained Detection of Smart Contract Vulnerabilities](https://mlsanity.com/paper/2208.13252/) (2022)
- [Automated Testing of COBOL to Java Transformation](https://mlsanity.com/paper/2504.10548/) (2025)
- [Statement-based Memory for Neural Source Code Summarization](https://mlsanity.com/paper/2307.11709/) (2023)
- [Dynamic Neural Control Flow Execution: An Agent-Based Deep Equilibrium Approach for Binary Vulnerability Detection](https://mlsanity.com/paper/2404.08562/) (2024)
- [Automated Validation of COBOL to Java Transformation](https://mlsanity.com/paper/2506.10999/) (2025)
- [DiffuTester: Accelerating Unit Test Generation for Diffusion LLMs via Mining Structural Pattern](https://mlsanity.com/paper/2509.24975/) (2025)
- [Program Analysis Guided LLM Agent for Proof-of-Concept Generation](https://mlsanity.com/paper/2604.07624/) (2026)
- [Neuro-Symbolic Execution of Generic Source Code](https://mlsanity.com/paper/2304.00989/) (2023)
- [AutoStub: Genetic Programming-Based Stub Creation for Symbolic Execution](https://mlsanity.com/paper/2509.08524/) (2025)
- [R1-Fuzz: Specializing Language Models for Textual Fuzzing via Reinforcement Learning](https://mlsanity.com/paper/2509.20384/) (2025)
- [Navigating the Labyrinth: Path-Sensitive Unit Test Generation with Large Language Models](https://mlsanity.com/paper/2509.23812/) (2025)
- [RAVEN: Agentic RAG for Automated Vulnerability Repair](https://mlsanity.com/paper/2606.22647/) (2026)
- [Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search](https://mlsanity.com/paper/2504.06542/) (2025)
- [Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models](https://mlsanity.com/paper/2509.13023/) (2025)
- [AutoEG: Exploiting Known Third-Party Vulnerabilities in Black-Box Web Applications](https://mlsanity.com/paper/2604.00704/) (2026)

## Abstract (arXiv)

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 last 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. The present survey has been accepted for publication at ACM Computing Surveys. If you are considering citing this survey, we would appreciate if you could use the following BibTeX entry: http://goo.gl/Hf5Fvc