Awesome

Symbolic Execution Papers

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

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

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)

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)

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)

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)

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)

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)

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