{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T23:34:31Z","timestamp":1770248071449,"version":"3.49.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["VIL4211"],"award-info":[{"award-number":["VIL4211"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Hong Kong PhD Fellowship Scheme","award":["PF20-52213"],"award-info":[{"award-number":["PF20-52213"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"\n Context-free language (CFL)<\/jats:italic>\n reachability is a standard approach in static analyses, where the analysis question (e.g., is there a dataflow from\n \n \n x<\/mml:mi>\n <\/mml:math>\n <\/jats:inline-formula>\n to\n \n \n y<\/mml:mi>\n <\/mml:math>\n <\/jats:inline-formula>\n ?) is phrased as a language reachability problem on a graph\n \n \n G<\/mml:mi>\n <\/mml:math>\n <\/jats:inline-formula>\n wrt a CFL\n \n \n L<\/mml:mi>\n <\/mml:math>\n <\/jats:inline-formula>\n . However, CFLs lack the expressiveness needed for high analysis precision. On the other hand, common formalisms for\n context-sensitive<\/jats:italic>\n languages are too expressive, in the sense that the corresponding reachability problem becomes undecidable.\n Are there useful context-sensitive language-reachability models for static analysis?<\/jats:italic>\n <\/jats:p>\n \n In this paper, we introduce\n Multiple Context-Free Language (MCFL)<\/jats:italic>\n reachability as an\n expressive<\/jats:italic>\n yet\n tractable<\/jats:italic>\n model for static program analysis. MCFLs form an infinite hierarchy of mildly context sensitive languages parameterized by a\n dimension<\/jats:italic>\n \n \n d<\/mml:mi>\n <\/mml:math>\n <\/jats:inline-formula>\n and a\n rank<\/jats:italic>\n \n \n r<\/mml:mi>\n <\/mml:math>\n <\/jats:inline-formula>\n . Larger\n \n \n d<\/mml:mi>\n <\/mml:math>\n <\/jats:inline-formula>\n and\n \n \n r<\/mml:mi>\n <\/mml:math>\n <\/jats:inline-formula>\n yield progressively more expressive MCFLs, offering\n tunable<\/jats:italic>\n 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.\n <\/jats:p>\n \n Given the increased expressiveness of MCFLs, one natural question pertains to their algorithmic complexity, i.e.,\n how fast can MCFL reachability be computed<\/jats:italic>\n ? We show that the problem takes\n \n \n \n O<\/mml:mi>\n \n \n \n n<\/mml:mi>\n \n 2<\/mml:mn>\n d<\/mml:mi>\n +<\/mml:mo>\n 1<\/mml:mn>\n <\/mml:mrow>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:mfenced>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n time on a graph of\n \n \n n<\/mml:mi>\n <\/mml:math>\n <\/jats:inline-formula>\n nodes when\n \n \n \n r<\/mml:mi>\n =<\/mml:mo>\n 1<\/mml:mn>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n , and\n \n \n \n O<\/mml:mi>\n \n \n \n n<\/mml:mi>\n \n d<\/mml:mi>\n \n \n r<\/mml:mi>\n +<\/mml:mo>\n 1<\/mml:mn>\n <\/mml:mrow>\n <\/mml:mfenced>\n <\/mml:mrow>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:mfenced>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n time when\n \n \n \n r<\/mml:mi>\n ><\/mml:mo>\n 1<\/mml:mn>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n . Moreover, we show that when\n \n \n \n r<\/mml:mi>\n =<\/mml:mo>\n 1<\/mml:mn>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n , even the simpler membership problem has a lower bound of\n \n \n \n \n n<\/mml:mi>\n \n 2<\/mml:mn>\n d<\/mml:mi>\n <\/mml:mrow>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n based on the Strong Exponential Time Hypothesis, while reachability for\n \n \n \n d<\/mml:mi>\n =<\/mml:mo>\n 1<\/mml:mn>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n has a lower bound of\n \n \n \n \n n<\/mml:mi>\n 3<\/mml:mn>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n based on the combinatorial Boolean Matrix Multiplication Hypothesis. Thus, for\n \n \n \n r<\/mml:mi>\n =<\/mml:mo>\n 1<\/mml:mn>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n , our algorithm is optimal within a factor\n \n \n n<\/mml:mi>\n <\/mml:math>\n <\/jats:inline-formula>\n for all levels of the hierarchy based on the dimension\n \n \n d<\/mml:mi>\n <\/mml:math>\n <\/jats:inline-formula>\n (and fully optimal for\n \n \n \n d<\/mml:mi>\n =<\/mml:mo>\n 1<\/mml:mn>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n ).\n <\/jats:p>\n \n We implement our MCFL reachability algorithm and evaluate it by underapproximating interleaved Dyck reachability for a standard taint analysis for Android. When combined with existing overapproximate methods, MCFL reachability discovers all tainted information on 8 out of 11 benchmarks, while it has remarkable coverage (confirming\n \n \n \n 94.3<\/mml:mn>\n %<\/mml:mtext>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n of the reachable pairs reported by the overapproximation) on the remaining 3. To our knowledge, this is the first report of high and provable coverage for this challenging benchmark set.\n <\/jats:p>","DOI":"10.1145\/3704854","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"509-538","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Program Analysis via Multiple Context Free Language Reachability"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9474-6505","authenticated-orcid":false,"given":"Giovanna Kobus","family":"Conrado","sequence":"first","affiliation":[{"name":"Hong Kong University of Science and Technology, Hong Kong, Hong Kong"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1275-9933","authenticated-orcid":false,"given":"Adam Husted","family":"Kjelstr\u00f8m","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-0625","authenticated-orcid":false,"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8943-0722","authenticated-orcid":false,"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"2003. T. J. Watson Libraries for Analysis (WALA). https:\/\/github.com\/wala\/WALA. Accessed: 2024-11-05."},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1075382.1075387"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38536-0_35"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646374"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2259051.2259052"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054196000191"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2021.106135"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158118"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3363525"},{"key":"e_1_3_2_11_1","unstructured":"Krishnendu Chatterjee Bernhard Kragl Samarth Mishra and Andreas Pavlogiannis. 2017. Faster Algorithms for Weighted Recursive State Machines. Vol. 10201. 287\u2013313. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_11 10.1007\/978-3-662-54434-1_11 arXiv:https:\/\/arxiv.org\/abs\/1701.04914 [cs]"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328460"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498702"},{"key":"e_1_3_2_14_1","unstructured":"Alexander Clark. 2014. An introduction to multiple context free grammars for linguists. https:\/\/alexc17.github.io\/static\/pdfs\/mcfgsforlinguists.pdf Accessed: 2024-11-05."},{"key":"e_1_3_2_15_1","unstructured":"Giovanna Kobus Conrado Adam Husted Kjelstr\u00f8m Andreas Pavlogiannis and Jaco van de Pol. 2024. Program Analysis via Multiple Context Free Language Reachability - Artifact. https:\/\/doi.org\/10.5281\/zenodo.13936483 10.5281\/zenodo.13936483"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3652588.3663318"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_12"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614960"},{"key":"e_1_3_2_20_1","unstructured":"Arthur Hicken. 2023. False Positives in Static Code Analysis. https:\/\/www.parasoft.com\/blog\/false-positives-in-static-code-analysis\/ Accessed: 2024-11-05."},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771803"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1075\/z.35.07jos"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571252"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02987162"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104588"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11688839_5"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571228"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360574"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926419"},{"key":"e_1_3_2_31_1","first-page":"29","volume-title":"Proc. ACM Program. Lang","author":"Mathiasen Anders Alnor","year":"2021","unstructured":"Anders Alnor Mathiasen and Andreas Pavlogiannis. 2021. The Fine-Grained and Parallel Complexity of Andersen\u2019s Pointer Analysis. Proc. ACM Program. Lang. 5, POPL, Article 34 (jan 2021), 29 pages. https:\/\/doi.org\/10.1145\/3434315 10.1145\/3434315"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428246"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3583660.3583664"},{"key":"e_1_3_2_34_1","volume-title":"Generalized Phrase Structure Grammars, Head Grammars, and Natural Language","author":"Pollard C.J.","year":"1984","unstructured":"C.J. Pollard. 1984. Generalized Phrase Structure Grammars, Head Grammars, and Natural Language. Stanford University. https:\/\/doi.org\/10.1007\/BF03037443 10.1007\/BF03037443"},{"key":"e_1_3_2_35_1","doi-asserted-by":"crossref","unstructured":"Psalm 2024. Psalm Documentation. https:\/\/psalm.dev\/docs\/security_analysis\/avoiding_false_positives Accessed: 2024-11-05.","DOI":"10.2307\/jj.20093331.18"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00190-4"},{"key":"e_1_3_2_38_1","doi-asserted-by":"crossref","unstructured":"Jakob Rehof and Manuel F\u00e4hndrich. 2001. Type-based Flow Analysis: From Polymorphic Subtyping to CFL-reachability. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 54\u201366. https:\/\/doi.org\/10.1145\/373243.360208 10.1145\/373243.360208","DOI":"10.1145\/360204.360208"},{"key":"e_1_3_2_39_1","first-page":"5","volume-title":"Proceedings of the 1997 International Symposium on Logic Programming (Port Washington, New York, USA) (ILPS \u201997)","author":"Reps Thomas","year":"1997","unstructured":"Thomas Reps. 1997. Program Analysis via Graph Reachability. In Proceedings of the 1997 International Symposium on Logic Programming (Port Washington, New York, USA) (ILPS \u201997). MIT Press, Cambridge, MA, USA, 5\u201319. https:\/\/doi.org\/10.5555\/271338.271343 10.5555\/271338.271343"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345137"},{"key":"e_1_3_2_41_1","first-page":"49","volume-title":"Precise interprocedural dataflow analysis via graph reachability (POPL \u201995)","author":"Reps Thomas","year":"1995","unstructured":"Thomas Reps, Susan Horwitz, and Mooly Sagiv. 1995. Precise interprocedural dataflow analysis via graph reachability (POPL \u201995). Association for Computing Machinery, New York, NY, USA, 49\u201361. https:\/\/doi.org\/10.1145\/199448.199462 10.1145\/199448.199462"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90374-B"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000014"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290361"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134027"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1103845.1094817"},{"key":"e_1_3_2_47_1","doi-asserted-by":"crossref","unstructured":"Yu Su Ding Ye and Jingling Xue. 2014. Parallel Pointer Analysis with CFL-Reachability. In 2014 43rd International Conference on Parallel Processing. 451\u2013460. https:\/\/doi.org\/10.1109\/ICPP.2014.54 10.1109\/ICPP.2014.54","DOI":"10.1109\/ICPP.2014.54"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_33"},{"key":"e_1_3_2_49_1","doi-asserted-by":"crossref","unstructured":"Salvatore La Torre Parthasarathy Madhusudan and Gennaro Parlato. 2007. A Robust Class of Context-Sensitive Languages. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007). 161\u2013170. https:\/\/doi.org\/10.1109\/LICS.2007.9 10.1109\/LICS.2007.9","DOI":"10.1109\/LICS.2007.9"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.3115\/981175.981190"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.023"},{"key":"e_1_3_2_52_1","doi-asserted-by":"crossref","unstructured":"Virginia Vassilevska Williams. [n. d.]. ON SOME FINE-GRAINED QUESTIONS IN ALGORITHMS AND COMPLEXITY. 3447\u20133487. https:\/\/doi.org\/10.1142\/9789813272880_0188 10.1142\/9789813272880_0188","DOI":"10.1142\/9789813272880_0188"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3186893"},{"key":"e_1_3_2_54_1","doi-asserted-by":"crossref","unstructured":"Harry Xu Atanas Rountev and Manu Sridharan. 2009. Scaling CFL-Reachability-Based Points-To Analysis Using Context-Sensitive Must-Not-Alias Analysis Vol. 5653. 98\u2013122. https:\/\/doi.org\/10.1007\/978-3-642-03013-0_6 10.1007\/978-3-642-03013-0_6","DOI":"10.1007\/978-3-642-03013-0_6"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/298514.298576"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009848"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704854","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704854","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:24Z","timestamp":1770200184000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704854"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704854"],"URL":"https:\/\/doi.org\/10.1145\/3704854","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}