# Prior Art (condensed)

Key papers grounding fold's design.

## Buffer overflow
- **Xu et al. (2020)** *ELAID.* doi:10.1186/s42400-020-00058-2 — interprocedural call graph + SMT on Juliet sinks.
- **Khedker (2014)** *Buffer Overflow Analysis.* arXiv:1412.5400 — buffer lattice with size + null-position sets.

## Dead code
- **Naug (2020)** *Useless Code Identification with SE.* doi:10.5373/jardcs/v12sp3/20201233 — dead-branch precedent.
- **Patil (2025)** *Opti-Blend.* doi:10.12732/ijam.v38i5.424 — unified framework for dead code + clones.

## Clones
- **Tronicek (2026)** *DrDupLex3.* doi:10.37190/e-inf260105 — Type-3 SOTA baseline.
- **Hummel et al. (2010)** *Index-based clone detection.* doi:10.1109/icsm.2010.5609665 — incremental clone caching.

## Code Property Graphs
- **Yamaguchi et al. (2014)** *Modeling Vulnerabilities with CPG.* doi:10.1109/sp.2014.44 — AST+CFG+PDG join.

## Null pointer analysis
- **Das & Lal (2017)** *GVN for null checking.* arXiv:1702.05807 — GVN makes alias analysis path-aware; the access-path/guarded-fact substrate is fold's analogue.
- **Estep et al. (2021)** *Gradual Program Analysis for Null Pointers.* arXiv:2105.06081 — gradual static/dynamic null analysis cuts FPs vs Infer; backs fold's `latent`/`precondition_required` tier for unguarded raw-pointer params (yams #13, #19).
- **Raad et al. (2020)** *Incorrectness Separation Logic.* doi:10.1007/978-3-030-53291-8_14 — under-approximate reasoning = no FP by construction; theory behind manifest-vs-latent reporting (Infer Pulse lineage).

## Recall lift
- **Gens et al. (2018)** *K-Miner.* NDSS. doi:10.14722/ndss.2018.23326 — kernel-scale interprocedural memory safety.
- **Miné (2007)** *Symbolic Methods for Numerical Abstract Domains.* — interval domain alongside BV.
- **Illous et al. (2020)** *Separation Logic Summaries.* doi:10.1007/978-3-030-65474-0_12 — pre/post summaries.
- **Zhang et al. (2025)** *CG-FSPTA.* arXiv:2508.01974 — flow-sensitive points-to without CFG.

## Heap model
- **Fischer et al. (2022)** *CBMC-SSM.* doi:10.1145/3551349.3559523 — symbolic shadow memory.
- **Feist et al. (2016)** *Finding the needle in the heap.* doi:10.1145/3015135.3015137 — UaF via static+SE.
- **Trabish et al. (2020)** *Past-sensitive pointer analysis.* doi:10.1145/3368089.3409698 — allocation-history disambiguation.
- **Nowack (2019)** *Fine-Grain Memory Object Representation.* doi:10.1109/ase.2019.00089 — granularity tradeoffs.

## Warning confirmation
- **Ma et al. (2011)** *Directed Symbolic Execution.* doi:10.1007/978-3-642-23702-7_11 — drive SE to targets.
- **Xu et al. (2025)** *Static Analysis Error Traces + DSE.* doi:10.1145/3713081.3731720 — scan→confirm architecture.
- **Gerasimov (2018)** *Directed Dynamic SE for Warning Confirmation.* doi:10.1134/s036176881805002x.
- **Shafiuzzaman et al. (2026)** *SAILOR: static-analysis-informed, LLM-orchestrated SE.* arXiv:2604.06506 — static targets → SE → concrete replay validation; 379 mem-safety bugs in 6.8M LOC. Mirrors fold's scan→confirm→fuzz-witness lane; motivates LLM-assisted `fuzz prep` harness synthesis.
- **Li et al. (2025)** *ColorGo: Directed Concolic Execution.* arXiv:2505.21130 — incremental coloration (static reachability + dynamic feasibility), 100× over AFLGo; directedness model for `fold confirm`/`fuzz`.

## Incremental SE
- **Yang et al. (2014)** *Directed Incremental SE.* doi:10.1145/2629536 — diff-guided exploration.
- **Yi & Yang (2022)** *Feedback-Driven Incremental SE.* doi:10.1109/issre55969.2022.00055 — feedback refinement.
- **Lin et al. (2016)** *Compositional SE: Incremental Solving Revisited.* doi:10.1109/apsec.2016.046 — solver reuse.

## Compositional summaries
- **Lin et al. (2015)** *Compositional SE Using Fine-Grained Summaries.* doi:10.1109/aswec.2015.32 — pre/post substitution.

## Foundations
- **Ferrante et al. (1987)** *The program dependence graph.* doi:10.1145/24039.24041 — PDG.
- **Braun et al. (2013)** *Simple Efficient SSA Construction.* doi:10.1007/978-3-642-37051-9_6.
- **Marashdih et al. (2022)** *SSA-based SE Abstraction.* doi:10.1007/s10515-022-00342-0.
- **de Moura & Bjørner (2008)** *Z3.* doi:10.1007/978-3-540-78800-3_24.
- **Bjørner et al. (2015)** *νZ.* doi:10.1007/978-3-319-21668-3_5 — push/pop, assumption-based solving.
- **Beyer (2016)** *BenchExec and Witnesses.* doi:10.1007/978-3-662-49674-9_55 — SV-COMP methodology.
- **Gadelha et al. (2018)** *ESBMC 5.0.* doi:10.1145/3238147.3240481 — comparable BMC.
- **Wagner & Sametinger (2014)** *Juliet comparison methodology.* doi:10.5220/0005032902440252.
- **Lenarduzzi et al. (2022)** *SonarQube precision.* doi:10.1007/s10664-022-10141-2 — FP induction rates.
- **Corbett et al. (2000)** *Bandera.* doi:10.1145/337180.337234 — predicate abstraction.

## Expression caching
- **Trabish et al. (2021)** *Address-Aware Query Caching.* doi:10.1109/icst49551.2021.00023 — canonical expression reuse.

## State merging / path explosion
- **Trabish et al. (2023)** *State Merging with Quantifiers in SE.* arXiv:2308.12068 — partitions states by uniform path-constraint structure and encodes merges with quantifiers, cutting disjunction/ITE blow-up; perf lever for fold's `states_merged` / `env_clone_ms` cost.
- **Bailey & Nicholas (2025)** *Symbolic Execution in Practice (survey).* arXiv:2508.06643 — taxonomy of scope-reduction vs guidance-heuristic strategies; anchor for the perf phase.

## FP triage / ranking
- **Ohlmer, Schlichtig & Bodden (2026)** *FP-Predictor.* arXiv:2603.10558 — GCN over Code Property Graphs classifies SAST reports TP/FP. fold already has IR + `FactProvenance` to build comparable features; candidate for a confidence-ranking lane.

## Datalog / DSL
- **Bembenek et al. (2020)** *Formulog.* arXiv:2009.08361 — Datalog+SMT for declarative detectors.