{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:50:22Z","timestamp":1790927422172,"version":"4.1.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>\n            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\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sub>\n            \u2299\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sub>\n            ) 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)\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            \u2299\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            reachability (i.e., when both Dyck languages are over a single parenthesis and act as counters) is computable in\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>7<\/jats:sup>\n            ) time, while (ii)\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sub>\n            \u2299\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sub>\n            reachability is NP-hard. However, despite this recent progress, most natural questions about this intricate problem are open.\n          <\/jats:p>\n          <jats:p>\n            In this work we address the decidability and complexity of all variants of interleaved bidirected Dyck reachability. First, we show that\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            \u2299\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            reachability can be computed in\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>3<\/jats:sup>\n            \u00b7 \u03b1(\n            <jats:italic>n<\/jats:italic>\n            )) time, significantly improving over the existing\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>7<\/jats:sup>\n            ) bound. Second, we show that\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sub>\n            \u2299\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            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\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sub>\n            \u2299\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            reachability where the counter remains linearly bounded. Our third result shows that this bounded variant can be solved in\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>2<\/jats:sup>\n            \u00b7 \u03b1(\n            <jats:italic>n<\/jats:italic>\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\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sub>\n            \u2299\n            <jats:italic>D<\/jats:italic>\n            <jats:sub>\n              <jats:italic>k<\/jats:italic>\n            <\/jats:sub>\n            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.\n          <\/jats:p>","DOI":"10.1145\/3498673","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["The decidability and complexity of interleaved bidirected Dyck reachability"],"prefix":"10.1145","volume":"6","author":[{"given":"Adam Husted","family":"Kjelstr\u00f8m","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8943-0722","authenticated-orcid":false,"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2003. T. J. Watson Libraries for Analysis (WALA). https:\/\/github.com.  2003. T. J. Watson Libraries for Analysis (WALA). https:\/\/github.com."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007352.1007390"},{"key":"e_1_2_2_3_1","volume-title":"Software Change Impact Analysis","author":"Arnold Robert S.","year":"1867","unstructured":"Robert S. Arnold . 1996. Software Change Impact Analysis . IEEE Computer Society Press , Los Alamitos, CA, USA . isbn:08 1867 3842 Robert S. Arnold. 1996. Software Change Impact Analysis. IEEE Computer Society Press, Los Alamitos, CA, USA. isbn:0818673842"},{"key":"e_1_2_2_4_1","volume-title":"Blackburn","author":"Stephen M.","year":"2006","unstructured":"Stephen M. et al. Blackburn . 2006 . The DaCapo Benchmarks: Java Benchmarking Development and Analysis. In OOPSLA. Stephen M. et al. Blackburn. 2006. The DaCapo Benchmarks: Java Benchmarking Development and Analysis. In OOPSLA."},{"key":"e_1_2_2_5_1","volume-title":"SOAP","author":"Bodden Eric","unstructured":"Eric Bodden . 2012. Inter-procedural Data-flow Analysis with IFDS\/IDE and Soot . In SOAP . ACM , New York, NY, USA . Eric Bodden. 2012. Inter-procedural Data-flow Analysis with IFDS\/IDE and Soot. In SOAP. ACM, New York, NY, USA."},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Phillip G. Bradford. 2018. Efficient Exact Paths For Dyck and semi-Dyck Labeled Path Reachability. arxiv:cs.DS\/1802.05239.  Phillip G. Bradford. 2018. Efficient Exact Paths For Dyck and semi-Dyck Labeled Path Reachability. arxiv:cs.DS\/1802.05239.","DOI":"10.1109\/UEMCON.2017.8249039"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2021.106135"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158118"},{"key":"e_1_2_2_9_1","volume-title":"Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.","author":"Chatterjee Krishnendu","year":"2020","unstructured":"Krishnendu Chatterjee , Amir Kafshdar Goharshady , Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. 2020 . Optimal and Perfectly Parallel Algorithms for On-demand Data-Flow Analysis. In Programming Languages and Systems, Peter M\u00fcller (Ed.). Springer International Publishing , Cham. 112\u2013140. isbn:978-3-030-44914-8 Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. 2020. Optimal and Perfectly Parallel Algorithms for On-demand Data-Flow Analysis. In Programming Languages and Systems, Peter M\u00fcller (Ed.). Springer International Publishing, Cham. 112\u2013140. isbn:978-3-030-44914-8"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676979"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_11"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328460"},{"key":"e_1_2_2_13_1","unstructured":"Dmitry Chistikov Rupak Majumdar and Philipp Schepper. 2021. Subcubic Certificates for CFL Reachability. arxiv:cs.FL\/2102.13095.  Dmitry Chistikov Rupak Majumdar and Philipp Schepper. 2021. Subcubic Certificates for CFL Reachability. arxiv:cs.FL\/2102.13095."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/773473.178263"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933577"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434298"},{"key":"e_1_2_2_17_1","doi-asserted-by":"crossref","unstructured":"Moses Ganardi Rupak Majumdar and Georg Zetzsche. 2021. The complexity of bidirected reachability in valence systems. arxiv:cs.FL\/2110.03654.  Moses Ganardi Rupak Majumdar and Georg Zetzsche. 2021. The complexity of bidirected reachability in valence systems. arxiv:cs.FL\/2110.03654.","DOI":"10.1145\/3531130.3533345"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/788019.788876"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771803"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.37"},{"key":"e_1_2_2_21_1","unstructured":"Adam Husted Kjelstr\u00f8m and Andreas Pavlogiannis. 2021. The Decidability and Complexity of Interleaved Bidirected Dyck Reachability. arxiv:cs.PL\/2111.05923. arxiv:2111.05923  Adam Husted Kjelstr\u00f8m and Andreas Pavlogiannis. 2021. The Decidability and Complexity of Interleaved Bidirected Dyck Reachability. arxiv:cs.PL\/2111.05923. arxiv:2111.05923"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.9"},{"key":"e_1_2_2_23_1","volume-title":"On Boundedness Problems for Pushdown Vector Addition Systems","author":"Leroux J\u00e9r\u00f4me","unstructured":"J\u00e9r\u00f4me Leroux , Gr\u00e9goire Sutre , and Patrick Totzke . 2015. On Boundedness Problems for Pushdown Vector Addition Systems . In Reachability Problems, Mikolai Bojanczyk, Slawomir Lasota, and Igor Potapov (Eds.). Springer International Publishing , Cham . 101\u2013113. isbn:978-3-319-24537-9 J\u00e9r\u00f4me Leroux, Gr\u00e9goire Sutre, and Patrick Totzke. 2015. On Boundedness Problems for Pushdown Vector Addition Systems. In Reachability Problems, Mikolai Bojanczyk, Slawomir Lasota, and Igor Potapov (Eds.). Springer International Publishing, Cham. 101\u2013113. isbn:978-3-319-24537-9"},{"key":"e_1_2_2_24_1","volume-title":"On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension","author":"Leroux J\u00e9r\u00f4me","unstructured":"J\u00e9r\u00f4me Leroux , Gr\u00e9goire Sutre , and Patrick Totzke . 2015. On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension . In Automata, Languages, and Programming, Magn\u00fas M. Halld\u00f3rsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 324\u2013336. isbn:978-3-662-47666-6 J\u00e9r\u00f4me Leroux, Gr\u00e9goire Sutre, and Patrick Totzke. 2015. On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension. In Automata, Languages, and Programming, Magn\u00fas M. Halld\u00f3rsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 324\u2013336. isbn:978-3-662-47666-6"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11688839_5"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386021"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434340"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360574"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926419"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434315"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428246"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90269-L"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360208"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/215465.215466"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/271338.271343"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345137"},{"key":"e_1_2_2_38_1","volume-title":"POPL","author":"Reps Thomas","unstructured":"Thomas Reps , Susan Horwitz , and Mooly Sagiv . 1995. Precise Interprocedural Dataflow Analysis via Graph Reachability . In POPL . ACM , New York, NY, USA . Thomas Reps, Susan Horwitz, and Mooly Sagiv. 1995. Precise Interprocedural Dataflow Analysis via Graph Reachability. In POPL. ACM, New York, NY, USA."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/195274.195287"},{"key":"e_1_2_2_40_1","volume-title":"Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets","author":"Schmitz Sylvain","unstructured":"Sylvain Schmitz and Georg Zetzsche . 2019. Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets . In Reachability Problems, Emmanuel Filiot, Rapha\u00ebl Jungers, and Igor Potapov (Eds.). Springer International Publishing , Cham . 193\u2013201. isbn:978-3-030-30806-3 Sylvain Schmitz and Georg Zetzsche. 2019. Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets. In Reachability Problems, Emmanuel Filiot, Rapha\u00ebl Jungers, and Igor Potapov (Eds.). Springer International Publishing, Cham. 193\u2013201. isbn:978-3-030-30806-3"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2259016.2259050"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290361"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133255.1134027"},{"key":"e_1_2_2_45_1","doi-asserted-by":"crossref","unstructured":"Manu Sridharan Denis Gopan Lexin Shan and Rastislav Bod\u00edk. 2005. Demand-driven Points-to Analysis for Java. In OOPSLA.  Manu Sridharan Denis Gopan Lexin Shan and Rastislav Bod\u00edk. 2005. Demand-driven Points-to Analysis for Java. In OOPSLA.","DOI":"10.1145\/1094811.1094817"},{"key":"e_1_2_2_46_1","volume-title":"Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization","author":"Tang Hao","unstructured":"Hao Tang , Di Wang , Yingfei Xiong , Lingming Zhang , Xiaoyin Wang , and Lu Zhang . 2017. Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization . In Programming Languages and Systems, Hongseok Yang (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 880\u2013908. isbn:978-3-662-54434-1 Hao Tang, Di Wang, Yingfei Xiong, Lingming Zhang, Xiaoyin Wang, and Lu Zhang. 2017. Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization. In Programming Languages and Systems, Hongseok Yang (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 880\u2013908. isbn:978-3-662-54434-1"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00091"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.023"},{"key":"e_1_2_2_49_1","unstructured":"Virginia Vassilevska Williams. 2019. On some fine-grained questions in algorithms and complexity.  Virginia Vassilevska Williams. 2019. On some fine-grained questions in algorithms and complexity."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_6"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001440"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/298514.298576"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_13"},{"key":"e_1_2_2_54_1","doi-asserted-by":"crossref","unstructured":"Qirun Zhang Michael R. Lyu Hao Yuan and Zhendong Su. 2013. Fast Algorithms for Dyck-CFL-reachability with Applications to Alias Analysis. PLDI. ACM.  Qirun Zhang Michael R. Lyu Hao Yuan and Zhendong Su. 2013. Fast Algorithms for Dyck-CFL-reachability with Applications to Alias Analysis. PLDI. ACM.","DOI":"10.1145\/2491956.2462159"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009848"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328464"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498673","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498673","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498673"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498673"],"URL":"https:\/\/doi.org\/10.1145\/3498673","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}