Symbolic Execution Papers

This repository is for collecting and grouping the symbolic execution papers and opensource tools in recent years.

Table of Contents

• Summary
• Path Explosion
• Memory Model
• Constraint Solving
• Environment Interaction
• Hybrid Fuzzing
• Engine
• Others

Summary

• 1976 Symbolic Execution and Program Testing

• 2010 All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)

• 2013 Symbolic Execution for Software Testing: Three Decades Later

• 2016 On the Techniques We Create, the Tools We Build, and Their Misalignments: A Study of KLEE

• 2018 A Survey of Symbolic Execution Techniques

Path Explosion

• 2011 Directed Incremental Symbolic Execution

• 2015 Under-Constrained Symbolic Execution Correctness Checking for Real Code

• 2018 Chopped Symbolic Execution (chopper)

• 2018 Automatically Generating Search Heuristics for Concolic Testing (ParaDySE)

• 2019 Concolic Testing with Adaptively Changing Search Heuristics (Chameleon)

• 2020 Efficient Multiplex Symbolic Execution with Adaptive Search Strategy

• 2020 Making Symbolic Execution Promising by Learning Aggressive State-Pruning Strategy (HOMI)

• 2020 Analyzing System Software Components using API Model Guided Symbolic Execution

• 2021 SyML: Guiding Symbolic Execution Toward Vulnerable States Through Pattern Learning (SyML)

• 2021 Learning to Explore Paths for Symbolic Execution (LEARCH)

• 2021 Metrinome: Path Complexity Predicts Symbolic Execution Path Explosion (Metrinome)

• 2021 TracerX: Dynamic Symbolic Execution with Interpolation (TraceX)

• 2022 Ferry: State-Aware Symbolic Execution for Exploring State-Dependent Program Paths

• 2022 Combining Static Analysis Error Traces with Dynamic Symbolic Execution (KLEE-sa)

• 2024 Concrete Constraint Guided Symbolic Execution (cgs)

• 2024 Marco: A Stochastic and Asynchronous Concolic Explorer

• 2024 Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding

• 2024 FeatMaker: Automated Feature Engineering for Search Strategy of Symbolic Execution (FeatMaker)

• 2024 Sparse Symbolic Loop Execution (Registered Report)

Constraint Solving

• 2019 Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints

• 2019 Enhancing Symbolic Execution by Machine Learning Based Solver Selection (PCC)

• 2019 Constraints in Dynamic Symbolic Execution: Bitvectors or Integers? (Data)

• 2019 Just Fuzz It Solving Floating-Point Constraints using Coverage-Guided Fuzzing (JFS)

• 2020 Pending Constraints in Symbolic Execution for Better Exploration and Seeding (Pending)

• 2020 Multiplex Symbolic Execution Exploring Multiple Paths by Solving Once

• 2021 Type and Interval Aware Array Constraint Solving for Symbolic Execution

• 2021 Synthesize Solving Strategy for Symbolic Execution

• 2021 Boosting Symbolic Execution via Constraint Solving Time Prediction (SMTimer)

• 2021 Address-Aware Query Caching for Symbolic Execution (KLEE-aaqc)

• 2022 Satisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing

• 2023 Intelligent Constraint Classification for Symbolic Execution

• 2023 Speeding up SMT Solving via Compiler Optimization

• 2024 Partial Solution Based Constraint Solving Cache in Symbolic Execution

• 2024 SMTTheory Arbitrage: Approximating Unbounded Constraints using Bounded Theories (STAUB)

Memory Model

• 2017 Rethinking pointer reasoning in symbolic execution (MEMSIGHT)

• 2019 Fine-grain Memory Object Representation in Symbolic Execution

• 2019 A Segmented Memory Model for Symbolic Execution

• 2020 Relocatable addressing model for symbolic execution (KLEE-ram)

• 2020 Past-Sensitive Pointer Analysis for Symbolic Execution (KLEE-pspa)

• 2021 A Bounded Symbolic-Size Model for Symbolic Execution (KLEE-symsize)

• 2022 A Deterministic Memory Allocator for Dynamic Symbolic Execution

• 2023 KDAlloc: The KLEE Deterministic Allocator (KDAlloc)

• 2024 Concretely Mapped Symbolic Memory Locations for Memory Error Detection (SymLoc)

Environment Interaction

• 2018 Avatar2: A Multi-target Orchestration Platform (Avatar2)

• 2020 SYMBION: Interleaving Symbolic with Concrete Execution (SYMBION)

• 2020 Mousse: A System for Selective Symbolic Execution of Programs with Untamed (Mousse)

• 2020 Device-agnostic Firmware Execution is Possible: A Concolic Execution Approach for Peripheral Emulation (Laelaps)

• 2021 Automatic Firmware Emulation through Invalidity-guided Knowledge Inference (uEmu)

• 2021 Jetset: Targeted Firmware Rehosting for Embedded Systems (Jetset)

• 2022 Fuzzware: Using Precise MMIO Modeling for Effective Firmware Fuzzing (Fuzzware)

Hybrid Fuzzing

• 2016 Driller: Augmenting Fuzzing Through Selective Symbolic Execution (Driller)

• 2019 Intriguer: Field-Level Constraint Solving for Hybrid Fuzzing (Intriguer)

• 2019 Matryoshka: Fuzzing Deeply Nested Branches

• 2019 Send Hardest Problems My Way: Probabilistic Path Prioritization for Hybrid Fuzzing (DigFuzz)

• 2019 Grey-box Concolic Testing on Binary Code (Eclipser)

• 2020 PANGOLIN: Incremental Hybrid Fuzzing with Polyhedral Path Abstraction

• 2020 SAVIOR: Towards Bug-Driven Hybrid Testing (SAVIOR)

• 2021 Fuzzing Symbolic Expressions (FUZZY-SAT)

• 2021 LeanSym: Efficient Hybrid Fuzzing Through Conservative Constraint Debloating

• 2022 JIGSAW: Efficient and Scalable Path Constraints Fuzzing (JIGSAW)

• 2022 CONFETTI: Amplifying Concolic Guidance for Fuzzers (CONFETTI)

• 2022 Sydr-Fuzz: Continuous Hybrid Fuzzing and Dynamic Analysis for Security Development Lifecycle (Sydr-Fuzz)

• 2023 Evaluating and Improving Hybrid Fuzzing (CoFuzz)

• 2023 Triereme: Speeding up hybrid fuzzing through efficient query scheduling (Triereme)

Engine

• 2008 KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs (KLEE)

• 2011 S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems (S2E)

• 2016 (State of) The Art of War: Offensive Techniques in Binary Analysis (Angr)

• 2018 QSYM: A Practical Concolic Execution Engine (QSYM)

• 2020 Symbolic execution with SymCC: Don't interpret, compile! (SymCC)

• 2021 SymQEMU: Compilation-based symbolic execution for binaries (SymQEMU)

• 2021 On the Feasibility of Automated Built-in Function Modeling for PHP Symbolic Execution

• 2022 SYMSAN: Time and Space Efficient Concolic Execution via Dynamic Data-flow Analysis (SYMSAN)

• 2022 SymFusion: Hybrid Instrumentation for Concolic Execution (SymFusion)

• 2022 SIFT: A Tool for Property Directed Symbolic Execution of Multithreaded Software (SIFT)

• 2022 SolSEE: A Source-Level Symbolic Execution Engine for Solidity(SolSEE)

• 2022 SYMBEXCEL: Automated Analysis and Understanding of Malicious Excel 4.0 Macros (SYMBEXCEL)

• 2023 GenSym: Compiling Parallel Symbolic Execution with Continuations (GenSym)

• 2023 KRover: A Symbolic Execution Engine for Dynamic Kernel Analysis

• 2024 SymFit: Making the Common (Concrete) Case Fast for Binary-Code Concolic Execution (SymFit)

• 2024 Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly (Owi)

• 2024 Holistic Concolic Execution for Dynamic Web Applications via Symbolic Interpreter Analysis (SymPHP)

Others

• 2019 Computing Summaries of String Loops in C for Better Testing and Refacto (KLEE-loops)

• 2019 Systematic Comparison of Symbolic Execution Systems: Intermediate Representation and its Generation (Data)

• 2019 Deferred Concretization in Symbolic Execution via Fuzzing

• 2020 Running Symbolic Execution Forever (MoKLEE)

• 2021 TASE: Reducing Latency of Symbolic Execution with Transactional Memory

• 2022 SymTuner: Maximizing the Power of Symbolic Execution by Adaptively Tuning External Parameters (SymTuner)

• 2022 Characterizing and Improving Bug-Finders with Synthetic Bugs

• 2022 Can symbolic execution be a productivity multiplier for human bug-finders?

• 2022 Symbolic Execution for Randomized Programs