{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:53:34Z","timestamp":1781855614266,"version":"3.54.5"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1917924,1420866"],"award-info":[{"award-number":["1917924,1420866"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2889,N00014-19-1-2318"],"award-info":[{"award-number":["N00014-17-1-2889,N00014-19-1-2318"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"\n Many program analyses need to reason about pairs of matching actions, such as call\/return, lock\/unlock, or set-field\/get-field. The family of Dyck languages {\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n }, where\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n has\n k<\/jats:italic>\n kinds of parenthesis pairs, can be used to model matching actions as balanced parentheses. Consequently, many program-analysis problems can be formulated as Dyck-reachability problems on edge-labeled digraphs.\n Interleaved Dyck-reachability<\/jats:italic>\n (InterDyck-reachability), denoted by\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n \u2299\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n -reachability, is a natural extension of Dyck-reachability that allows one to formulate program-analysis problems that involve\n multiple<\/jats:italic>\n kinds of matching-action pairs. Unfortunately, the general InterDyck-reachability problem is undecidable.\n <\/jats:p>\n \n In this paper, we study variants of InterDyck-reachability on\n bidirected graphs<\/jats:italic>\n , where for each edge \u27e8\n p<\/jats:italic>\n ,\n q<\/jats:italic>\n \u27e9 labeled by an open parenthesis \u201d(\n \n a<\/jats:italic>\n <\/jats:sub>\n \u201d, there is an edge \u27e8\n q<\/jats:italic>\n ,\n p<\/jats:italic>\n \u27e9 labeled by the corresponding close parenthesis \u201d)\n \n a<\/jats:italic>\n <\/jats:sub>\n \u201d, and\n vice versa<\/jats:italic>\n . Language-reachability on a bidirected graph has proven to be useful both (1) in its own right, as a way to formalize many program-analysis problems, such as pointer analysis, and (2) as a\n relaxation<\/jats:italic>\n method that uses a fast algorithm to over-approximate language-reachability on a directed graph. However, unlike its directed counterpart, the complexity of bidirected InterDyck-reachability still remains open.\n <\/jats:p>\n \n We establish the first decidable variant (i.e.,\n D<\/jats:italic>\n 1<\/jats:sub>\n \u2299\n D<\/jats:italic>\n 1<\/jats:sub>\n -reachability) of bidirected InterDyck-reachability. In\n D<\/jats:italic>\n 1<\/jats:sub>\n \u2299\n D<\/jats:italic>\n 1<\/jats:sub>\n -reachability, each of the two Dyck languages is restricted to have only a single kind of parenthesis pair. In particular, we show that the bidirected\n D<\/jats:italic>\n 1<\/jats:sub>\n \u2299\n D<\/jats:italic>\n 1<\/jats:sub>\n problem is in PTIME. We also show that when one extends each Dyck language to involve\n k<\/jats:italic>\n different kinds of parentheses (i.e.,\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n \u2299\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n -reachability with\n k<\/jats:italic>\n \u2265 2), the problem is NP-hard (and therefore much harder).\n <\/jats:p>\n \n We have implemented the polynomial-time algorithm for bidirected\n D<\/jats:italic>\n 1<\/jats:sub>\n \u2299\n D<\/jats:italic>\n 1<\/jats:sub>\n -reachability.\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n \u2299\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n -reachability provides a new over-approximation method for bidirected\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n \u2299\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n -reachability in the sense that\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n \u2299\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n -reachability can first be relaxed to bidirected\n D<\/jats:italic>\n 1<\/jats:sub>\n \u2299\n D<\/jats:italic>\n 1<\/jats:sub>\n -reachability, and then the resulting bidirected\n D<\/jats:italic>\n 1<\/jats:sub>\n \u2299\n D<\/jats:italic>\n 1<\/jats:sub>\n -reachability problem is solved precisely. We compare this\n D<\/jats:italic>\n 1<\/jats:sub>\n \u2299\n D<\/jats:italic>\n 1<\/jats:sub>\n -reachability-based approach against another known over-approximating\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n \u2299\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n -reachability algorithm. Surprisingly, we found that the over-approximation approach based on bidirected\n D<\/jats:italic>\n 1<\/jats:sub>\n \u2299\n D<\/jats:italic>\n 1<\/jats:sub>\n -reachability computes\n more precise<\/jats:italic>\n solutions, even though the\n D<\/jats:italic>\n 1<\/jats:sub>\n \u2299\n D<\/jats:italic>\n 1<\/jats:sub>\n formalism is inherently less expressive than the\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n \u2299\n D<\/jats:italic>\n \n k<\/jats:italic>\n <\/jats:sub>\n formalism.\n <\/jats:p>","DOI":"10.1145\/3434340","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["On the complexity of bidirected interleaved Dyck-reachability"],"prefix":"10.1145","volume":"5","author":[{"given":"Yuanbo","family":"Li","sequence":"first","affiliation":[{"name":"Georgia Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qirun","family":"Zhang","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594299"},{"key":"e_1_2_1_2_1","first-page":"169","article-title":"The DaCapo Benchmarks: Java Benchmarking Development and Analysis. In OOPSLA '06","author":"Blackburn S. M.","year":"2006","unstructured":"S. M. Blackburn, R. Garner, C. Hofman, A. M. Khan, K. S. McKinley, R. Bentzur, A. Diwan, D. Feinberg, D. Frampton, S. Z. Guyer, M. Hirzel, A. Hosking, M. Jump, H. Lee, J. E. B. Moss, A. Phansalkar, D. Stefanovi\u0107, T. VanDrunen, D. von Dincklage, and B. Wiedermann. 2006. The DaCapo Benchmarks: Java Benchmarking Development and Analysis. In OOPSLA '06: Proceedings of the 21st annual ACM SIGPLAN conference on Object-Oriented Programing, Systems, Languages, and Applications. 169-190.","journal-title":"Proceedings of the 21st annual ACM SIGPLAN conference on Object-Oriented Programing, Systems, Languages, and Applications."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158118"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328460"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2000 ). ACM, 57-69","author":"Cheng Ben-Chung","unstructured":"Ben-Chung Cheng and Wen-mei W. Hwu. 2000. Modular interprocedural pointer analysis using access paths: design, implementation, and evaluation. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2000 ). ACM, 57-69."},{"key":"e_1_2_1_6_1","article-title":"On Two Problems in the Generation of Program Test Paths","volume":"2","author":"Gabow Harold N.","year":"1976","unstructured":"Harold N. Gabow, Shachindra N. Maheswari, and Leon J. Osterweil. 1976. On Two Problems in the Generation of Program Test Paths. IEEE Trans. Software Eng. 2, 3 ( 1976 ), 227-231.","journal-title":"IEEE Trans. Software Eng."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771803"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.45"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996867"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1089\/cmb.2013.0004"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386021"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926419"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345137"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290361"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134027"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094817"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_6"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001440"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009848"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434340","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434340","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434340","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:29:46Z","timestamp":1781854186000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434340"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":22,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434340"],"URL":"https:\/\/doi.org\/10.1145\/3434340","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}