{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:17:28Z","timestamp":1767928648357,"version":"3.49.0"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T00:00:00Z","timestamp":1664582400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM SIGLOG News"],"published-print":{"date-parts":[[2022,10]]},"abstract":"<jats:p>\n            CFL\/Dyck reachability is a simple graph-theoretic problem: given a CFL\/Dyck language\n            <jats:italic>L<\/jats:italic>\n            over an alphabet \u03a3, a graph\n            <jats:italic>G<\/jats:italic>\n            = (\n            <jats:italic>V<\/jats:italic>\n            ,\n            <jats:italic>E<\/jats:italic>\n            ) of \u03a3-labeled edges, and two distinguished nodes\n            <jats:italic>s<\/jats:italic>\n            ,\n            <jats:italic>t<\/jats:italic>\n            \u2208\n            <jats:italic>V<\/jats:italic>\n            , does there exist a path from\n            <jats:italic>s<\/jats:italic>\n            to\n            <jats:italic>t<\/jats:italic>\n            that spells out a word in\n            <jats:italic>L<\/jats:italic>\n            ? This simple notion of language-based graph reachability serves as the algorithmic formulation of a large number of problems in diverse domains, such as graph databases and program static analysis. This paper takes an algorithmic perspective on CFL\/Dyck reachability, and overviews several recent advances concerning the decidability and complexity of the problem and some its close variants, as realized in the areas of automata theory and program verification.\n          <\/jats:p>","DOI":"10.1145\/3583660.3583664","type":"journal-article","created":{"date-parts":[[2023,2,6]],"date-time":"2023-02-06T17:06:21Z","timestamp":1675703181000},"page":"5-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["CFL\/Dyck Reachability"],"prefix":"10.1145","volume":"9","author":[{"given":"Andreas","family":"Pavlogiannis","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2023,2,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(68)91087-5"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007352.1007390"},{"key":"e_1_2_1_3_1","volume-title":"Doklady Akademii Nauk","volume":"194","author":"Arlazarov Vladimir L'vovich","year":"1970","unstructured":"Vladimir L'vovich Arlazarov , Yefim A Dinitz , MA Kronrod , and IgorAleksandrovich Faradzhev . 1970 . On economical construction of the transitive closure of an oriented graph . In Doklady Akademii Nauk , Vol. 194 . Russian Academy of Sciences, 487--488. Vladimir L'vovich Arlazarov, Yefim A Dinitz, MA Kronrod, and IgorAleksandrovich Faradzhev. 1970. On economical construction of the transitive closure of an oriented graph. In Doklady Akademii Nauk, Vol. 194. Russian Academy of Sciences, 487--488."},{"key":"e_1_2_1_4_1","volume-title":"Software Change Impact Analysis","author":"Arnold Robert S.","unstructured":"Robert S. Arnold . 1996. Software Change Impact Analysis . IEEE Computer Society Press , Los Alamitos, CA, USA . Robert S. Arnold. 1996. Software Change Impact Analysis. IEEE Computer Society Press, Los Alamitos, CA, USA."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(80)90001-0"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2840728.2840746"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2021.106135"},{"key":"e_1_2_1_8_1","volume-title":"Proc. ACM Program. Lang. 2, POPL, Article Article 30 (Dec.","author":"Chatterjee Krishnendu","year":"2018","unstructured":"Krishnendu Chatterjee , Bhavya Choudhary , and Andreas Pavlogiannis . 2018 . Optimal Dyck Reachability for Data-Dependence and Alias Analysis . Proc. ACM Program. Lang. 2, POPL, Article Article 30 (Dec. 2018), 30 pages. Krishnendu Chatterjee, Bhavya Choudhary, and Andreas Pavlogiannis. 2018. Optimal Dyck Reachability for Data-Dependence and Alias Analysis. Proc. ACM Program. Lang. 2, POPL, Article Article 30 (Dec. 2018), 30 pages."},{"key":"e_1_2_1_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--140. 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--140."},{"key":"e_1_2_1_10_1","volume-title":"Amir Kafshdar Goharshady, and Andreas Pavlogiannis","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee , Amir Kafshdar Goharshady, and Andreas Pavlogiannis . 2017 . JTDec: A Tool for Tree Decompositions in Soot. In Automated Technology for Verification and Analysis, Deepak D'Souza and K. Narayan Kumar (Eds.). Springer International Publishing , Cham, 59--66. Krishnendu Chatterjee, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. 2017. JTDec: A Tool for Tree Decompositions in Soot. In Automated Technology for Verification and Analysis, Deepak D'Souza and K. Narayan Kumar (Eds.). Springer International Publishing, Cham, 59--66."},{"key":"e_1_2_1_11_1","volume-title":"24th Annual European Symposium on Algorithms, ESA 2016","author":"Chatterjee Krishnendu","year":"2016","unstructured":"Krishnendu Chatterjee , Rasmus Ibsen-Jensen , and Andreas Pavlogiannis . 2016 . Optimal Reachability and a Space-Time Tradeoff for Distance Queries in Constant-Treewidth Graphs . In 24th Annual European Symposium on Algorithms, ESA 2016 , August 22 --24 , 2016, Aarhus, Denmark. 28:1--28:17. Krishnendu Chatterjee, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. 2016. Optimal Reachability and a Space-Time Tradeoff for Distance Queries in Constant-Treewidth Graphs. In 24th Annual European Symposium on Algorithms, ESA 2016, August 22--24, 2016, Aarhus, Denmark. 28:1--28:17."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676979"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328460"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498702"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)72023-8"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90158-1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933577"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2022.124"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/788019.788876"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/568438.568455"},{"key":"e_1_2_1_22_1","volume-title":"Ullman","author":"Hopcroft John E.","year":"2006","unstructured":"John E. Hopcroft , Rajeev Motwani , and Jeffrey D . Ullman . 2006 . Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley Longman Publishing Co. , Inc., USA. John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. 2006. Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley Longman Publishing Co., Inc., USA."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771803"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498673"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/505241.505242"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/3470152.3470202"},{"key":"e_1_2_1_27_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--336. 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--336."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 15th International Conference on Compiler Construction (CC). 47--64","author":"Lhot\u00e1k Ond\u0159ej","year":"2006","unstructured":"Ond\u0159ej Lhot\u00e1k and Laurie Hendren . 2006 . Context-Sensitive Points-to Analysis: Is It Worth It? . In Proceedings of the 15th International Conference on Compiler Construction (CC). 47--64 . Ond\u0159ej Lhot\u00e1k and Laurie Hendren. 2006. Context-Sensitive Points-to Analysis: Is It Worth It?. In Proceedings of the 15th International Conference on Compiler Construction (CC). 47--64."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434315"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/800076.802477"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428246"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90269-L"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 54--66","author":"Rehof Jakob","year":"2001","unstructured":"Jakob Rehof and Manuel F\u00e4hndrich . 2001 . Type-base Flow Analysis: From Polymorphic Subtyping to CFL-reachability . In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 54--66 . Jakob Rehof and Manuel F\u00e4hndrich. 2001. Type-base Flow Analysis: From Polymorphic Subtyping to CFL-reachability. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 54--66."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/215465.215466"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/271338.271343"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345137"},{"key":"e_1_2_1_37_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_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/195274.195287"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0095-8956(83)90079-5"},{"key":"e_1_2_1_40_1","volume-title":"Combinatorial Algorithms on Words","author":"Rytter Wojciech","unstructured":"Wojciech Rytter . 1985. The Complexity of Two-Way Pushdown Automata and Recursive Programs . In Combinatorial Algorithms on Words , Alberto Apostolico and Zvi Galil (Eds.). Springer Berlin Heidelberg, Berlin , Heidelberg , 341--356. Wojciech Rytter. 1985. The Complexity of Two-Way Pushdown Automata and Recursive Programs. In Combinatorial Algorithms on Words, Alberto Apostolico and Zvi Galil (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 341--356."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80024-3"},{"key":"e_1_2_1_42_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--201. 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--201."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290361"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133255.1134027"},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 16th International Symposium on Static Analysis (SAS '09)","author":"Sridharan Manu","unstructured":"Manu Sridharan and Stephen J. Fink . 2009. The Complexity of Andersen's Analysis in Practice . In Proceedings of the 16th International Symposium on Static Analysis (SAS '09) . Springer-Verlag, Berlin, Heidelberg, 205--221. Manu Sridharan and Stephen J. Fink. 2009. The Complexity of Andersen's Analysis in Practice. In Proceedings of the 16th International Symposium on Static Analysis (SAS '09). Springer-Verlag, Berlin, Heidelberg, 205--221."},{"key":"e_1_2_1_46_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_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1963405.1963491"},{"key":"e_1_2_1_48_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--908. 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--908."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90042-4"},{"key":"e_1_2_1_50_1","volume-title":"All Structured Programs Have Small Tree Width and Good Register Allocation. Information and Computation","author":"Thorup Mikkel","year":"1998","unstructured":"Mikkel Thorup . 1998. All Structured Programs Have Small Tree Width and Good Register Allocation. Information and Computation ( 1998 ). Mikkel Thorup. 1998. All Structured Programs Have Small Tree Width and Good Register Allocation. Information and Computation (1998)."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(75)80046-8"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00091"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_6"},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the 2011 International Symposium on Software Testing and Analysis (ISSTA). 155--165","author":"Yan Dacong","year":"2011","unstructured":"Dacong Yan , Guoqing Xu , and Atanas Rountev . 2011 . Demand-driven Context-sensitive Alias Analysis for Java . In Proceedings of the 2011 International Symposium on Software Testing and Analysis (ISSTA). 155--165 . Dacong Yan, Guoqing Xu, and Atanas Rountev. 2011. Demand-driven Context-sensitive Alias Analysis for Java. In Proceedings of the 2011 International Symposium on Software Testing and Analysis (ISSTA). 155--165."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_13"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462159"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328464"}],"container-title":["ACM SIGLOG News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3583660.3583664","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3583660.3583664","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:54Z","timestamp":1750178274000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3583660.3583664"}},"subtitle":["An Algorithmic Perspective"],"short-title":[],"issued":{"date-parts":[[2022,10]]},"references-count":57,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,10]]}},"alternative-id":["10.1145\/3583660.3583664"],"URL":"https:\/\/doi.org\/10.1145\/3583660.3583664","relation":{},"ISSN":["2372-3491"],"issn-type":[{"value":"2372-3491","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10]]},"assertion":[{"value":"2023-02-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}