paper_title=Concrete Constraint Guided Symbolic Execution
authors=Yue Sun; Guowei Yang; Shichao Lv; Zhi Li; Limin Sun
venue=ICSE 2024
doi=https://doi.org/10.1145/3597503.3639078
artifact_evaluation=https://conf.researchr.org/details/icse-2024/icse-2024-artifact-evaluation/3/Concrete-Constraint-Guided-Symbolic-Execution
artifact_archive=https://zenodo.org/records/10516325
author_repository_commit=7cf3890d80df12660255d81a8b50945cf1cc85a3
preprint_sha256=91b85536eb9410eed2d019dee1dd884df6b5207419c9e83f925941af25e63969
inspected_paper=Algorithms 1-3; concrete branch/store dependency; target update; evaluation boundary
inspected_artifact=klee/lib/Core/Searcher.cpp CGSSearcher; klee/lib/Core/Executor.cpp concrete branch/store events and options; IDA static dependency implementation
artifact_target_branch_num_default=10
artifact_target_branch_reach_max_default=64
artifact_target_update_help_text=500000 instructions
artifact_target_update_actual_init=1000000 instructions
artifact_queue_semantics=branch_states FIFO before ordinary states FIFO
adaptation_scope=exact function-local fixed-address unguarded width-matched store-load-icmp; identity chain; one AND/OR mask; signed/unsigned bit-vector predicates
adaptation_persistence=content-addressed store markers; snapshot v5; lease-fenced ordered event replay; deterministic rotation
fail_open=symbolic address/value; guarded/overlapping store; memory-affecting call; ambiguous SSA/site/token; unsupported expression; analysis budget
claim_boundary=synthetic mechanism target latency only; no artifact-equivalence, public campaign, completeness, solver-speedup, coverage-gain, or bug-yield claim