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

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

• 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)

• 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)

• 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

• 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)

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

• 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)

• 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)

• 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)

• 2020 Running Symbolic Execution Forever (MoKLEE)

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

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

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

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

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

• 2022 Characterizing and Improving Bug-Finders with Synthetic Bugs

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

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

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