Replication package for "MemPath: Feasibility-Aware Bounded Search for Paths with Maximum Memory-Access Count in C"

Static identification of costly feasible executions is useful before a final processor or timing model is available, but it must not be confused with cycle-accurate worst-case execution-time (WCET) analysis. This paper presents MemPath, a source-level analyzer that searches bounded C executions for a feasible path maximizing a source-level memory-access count M. Its prefix-keyed search (PKS) keys each state by control-flow-graph (CFG) location, loop counters, and the full event prefix, scores only complete paths with a satisfiability-modulo-theories (SMT) path evaluator shared with an exhaustive depth-first search (DFS) reference, and prunes a prefix only when its path condition is proved unsatisfiable. We prove bounded optimality, show that this key admits no state reuse, and use an independent-guard example to illustrate when exact suffix dynamic programming can be sound. On 20 controlled subjects, the PKS witness agrees with DFS and with independent concrete execution in all 210 defined executions. A 32-program historical regression has no completed mismatch (23 complete, nine time out). Of 193 collected corpus programs, 166 (233 functions) complete both PKS and DFS with identical maxima. For 66 small-library slices, function summaries yield 20 positive estimates, none from the 30 slices that retain the original body; on 36 fixed-input path witnesses from six projects, the analyzer's per-path counts match