Interleaved Dyck reachability is a standard, graph-based formulation of a plethora of static analyses that seek to be context- and field-sensitive, where each type of sensitivity is expressed via a CFL/Dyck language. Unfortunately, the problem is well-known to be undecidable in general, and as such, existing approaches resort on clever overapproximations. Recently, a mutual-refinement algorithm, that iteratively considers each of the two sensitivities in isolation until a fixpoint, was shown to achieve high precision.

In this work we present a more precise approximation of interleaved Dyck reachability, by extending the mutual-refinement algorithm in two directions. First, we develop refined CFLs to express each type of sensitivity precisely, while simultaneously also lightly overapproximating the opposite type. Second, we apply the resulting algorithm on an on-demand basis, which effectively masks out imprecision incurred by parts of the graph that are irrelevant for the query at hand. Our experiments show that the new approach offers significantly higher precision that the vanilla mutual-refinement algorithm and other common baselines.