Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Pro...
summary
Presents a single-source–single-target algorithm that summarizes all source→target paths as path expressions and reduces InterDyck reachability to a parenthesis-counting feasibility problem solved by integer linear programming. Implements the ILP pipeline, runs it on concurrency and taint benchmarks, and reports concrete wins: 1.42×, 28.24×, and 11.76× speedups over LCL, SPDS, and domain-specific tools on concurrency benchmarks (and similar improvements on taint), plus 4–11% precision gains; the implementation is practical and yields actual witnesses when ILP is feasible.
AI-written summary · about