{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:53:31Z","timestamp":1790927611214,"version":"4.1.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2889"],"award-info":[{"award-number":["N00014-17-1-2889"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1917924, 2114627, 2211968, 2212558"],"award-info":[{"award-number":["1917924, 2114627, 2211968, 2212558"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N66001-21-C-4024"],"award-info":[{"award-number":["N66001-21-C-4024"]}],"id":[{"id":"10.13039\/100000185","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":[[2023,1,9]]},"abstract":"<jats:p>An interleaved-Dyck (InterDyck) language consists of the interleaving of two or more Dyck languages, where each Dyck language represents a set of strings of balanced parentheses.InterDyck-reachability is a fundamental framework for program analyzers that simultaneously track multiple properly-matched pairs of actions such as call\/return, lock\/unlock, or write-data\/read-data.Existing InterDyck-reachability algorithms are based on the well-known tabulation technique.<\/jats:p>\n          <jats:p>\n            This paper presents a new perspective on solving InterDyck-reachability. Our key observation is that for the single-source-single-target InterDyck-reachability variant, it is feasible to summarize all paths from the source node to the target node based on\n            <jats:italic>path expressions<\/jats:italic>\n            . Therefore, InterDyck-reachability becomes an InterDyck-path-recognition problem over path expressions. Instead of computing summary edges as in traditional tabulation algorithms, this new perspective enables us to express InterDyck-reachability as a\n            <jats:italic>parenthesis-counting<\/jats:italic>\n            problem, which can be naturally formulated via integer linear programming (ILP).\n          <\/jats:p>\n          <jats:p>We implemented our ILP-based algorithm and performed extensive evaluations based on two client analyses (a reachability analysis for concurrent programs and a taint analysis). In particular, we evaluated our algorithm against two types of algorithms: (1) the general all-pairs InterDyck-reachability algorithms based on linear conjunctive language (LCL) reachability and synchronized pushdown system (SPDS) reachability, and (2) two domain-specific algorithms for both client analyses. The experimental results are encouraging. Our algorithm achieves 1.42\u00d7, 28.24\u00d7, and 11.76\u00d7 speedup for the concurrency-analysis benchmarks compared to all-pair LCL-reachability, SPDS-reachability, and domain-specific tools, respectively; 1.2\u00d7, 69.9\u00d7, and 0.98\u00d7 speedup for the taint-analysis benchmarks. Moreover, the algorithm also provides precision improvements, particularly for taint analysis, where it achieves 4.55%, 11.1%, and 6.8% improvement, respectively.<\/jats:p>","DOI":"10.1145\/3571228","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"1003-1026","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0194-5589","authenticated-orcid":false,"given":"Yuanbo","family":"Li","sequence":"first","affiliation":[{"name":"Georgia Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5367-9377","authenticated-orcid":false,"given":"Qirun","family":"Zhang","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594299"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3464794"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933577"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1997-3112"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26529-2_25"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2022.124"},{"key":"e_1_2_1_7_1","volume-title":"Monocopy and Associative Algorithms in an Extended LISP. Information Science Laboratory","author":"Goto E.","unstructured":"E. Goto . 1974. Monocopy and Associative Algorithms in an Extended LISP. Information Science Laboratory , Univ. of Tokyo . E. Goto. 1974. Monocopy and Associative Algorithms in an Extended LISP. Information Science Laboratory, Univ. of Tokyo."},{"key":"e_1_2_1_8_1","unstructured":"Gurobi Optimization LLC. 2021. Gurobi Optimizer Reference Manual. https:\/\/www.gurobi.com \t\t\t\t  Gurobi Optimization LLC. 2021. Gurobi Optimizer Reference Manual. https:\/\/www.gurobi.com"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/381694.378802"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(79)90041-0"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771803"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498673"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996867"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386021"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434340"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192419"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00049-9"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345137"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59293-8_226"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2893582.2893585"},{"key":"e_1_2_1_24_1","volume-title":"Theory of linear and integer programming","author":"Schrijver Alexander","unstructured":"Alexander Schrijver . 1998. Theory of linear and integer programming . John Wiley & Sons . Alexander Schrijver. 1998. Theory of linear and integer programming. John Wiley & Sons."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_94"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290361"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094817"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322273"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_25"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321719"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001440"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/298514.298576"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462159"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009848"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660213"},{"key":"e_1_2_1_36_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\/3571228","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571228","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571228"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":36,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571228"],"URL":"https:\/\/doi.org\/10.1145\/3571228","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}