Context-free language (CFL) reachability is a standard approach in static analyses, where the analysis question (e.g., is there a dataflow from x to y ?) is phrased as a language reachability problem on a graph G wrt a CFL L . However, CFLs lack the expressiveness needed for high analysis precision. On the other hand, common formalisms for context-sensitive languages are too expressive, in the sense that the corresponding reachability problem becomes undecidable. Are there useful context-sensitive language-reachability models for static analysis? In this paper, we introduce Multiple Context-Free Language (MCFL) reachability as an expressive yet tractable model for static program analysis. MCFLs form an infinite hierarchy of mildly context sensitive languages parameterized by a dimension d and a rank r . Larger d and r yield progressively more expressive MCFLs, offering tunable analysis precision. We showcase the utility of MCFL reachability by developing a family of MCFLs that approximate interleaved Dyck reachability, a common but undecidable static analysis problem. Given the increased expressiveness of MCFLs, one natural question pertains to their algorithmic complexity, i.e., how fast can MCFL reachability be computed ? We show that the problem takes O n 2 d + 1 time on a graph of n nodes when r = 1 , and O n d r + 1 time when r > 1 . Moreover, we show that when r = 1 , even the simpler membership problem has a lower bound of n 2 d based on the Strong Exponential Time Hypothesis, while reachability for d = 1 has a lower bound of n 3 based on the combinatorial Boolean Matrix Multiplication Hypothesis. Thus, for

Dyck reachability is the standard formulation of a large domain of static analyses, as it achieves the sweet spot between precision and efficiency, and has thus been studied extensively. Interleaved Dyck reachability (denoted D k ⊙ D k ) uses two Dyck languages for increased precision (e.g., context and field sensitivity) but is well-known to be undecidable. As many static analyses yield a certain type of bidirected graphs, they give rise to interleaved bidirected Dyck reachability problems. Although these problems have seen numerous applications, their decidability and complexity has largely remained open. In a recent work, Li et al. made the first steps in this direction, showing that (i) D 1 ⊙ D 1 reachability (i.e., when both Dyck languages are over a single parenthesis and act as counters) is computable in O ( n 7 ) time, while (ii) D k ⊙ D k reachability is NP-hard. However, despite this recent progress, most natural questions about this intricate problem are open. In this work we address the decidability and complexity of all variants of interleaved bidirected Dyck reachability. First, we show that D 1 ⊙ D 1 reachability can be computed in O ( n 3 · α( n )) time, significantly improving over the existing O ( n 7 ) bound. Second, we show that D k ⊙ D 1 reachability (i.e., when one language acts as a counter) is decidable, in contrast to the non-bidirected case where decidability is open. We further consider D k ⊙ D 1 reachability where the counter remains linearly bounded. Our third result shows that this bounded variant can be solved in O ( n 2 · α( n )) time, while our fourth result shows that the problem has a (conditional) quadratic lower bound, and thus our upper bound is essentially optimal. Fifth, we show that full D k ⊙ D k reachability is undecidable. This improves the recent NP-hardness lower-bound, and shows that the problem is equivalent to the non-bidirected case. Our experiments on standard benchmarks show that the new algorithms are very fast in practice, offering many orders-of-magnitude speedups over previous methods.

We consider the problem of reachability on One-Counter Systems (OCSs) and Pushdown Systems (PDSs). The problem has a well-known O(n3) bound on both models, while the bound is believed to be tight for PDSs. Here we establish new upper and lower bounds for reachability on OCSs and restricted PDSs. We show that the problem can be solved (i) in O(nω⋅log2⁡n) time on OCSs, and (ii) in O(n2) time on sparse PDSs when restricted to witness executions of stack height bounded by log⁡n. Moreover, we prove similar lower bounds.