{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T13:46:57Z","timestamp":1787060817375,"version":"build-2736575974"},"reference-count":63,"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\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["610150, 648701,725978"],"award-info":[{"award-number":["610150, 648701,725978"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660"],"award-info":[{"award-number":["389792660"]}],"id":[{"id":"10.13039\/501100001659","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":[[2022,1,16]]},"abstract":"<jats:p>\n                    Many problems in interprocedural program analysis can be modeled as the context-free language (CFL) reachability problem on graphs and can be solved in cubic time. Despite years of efforts, there are no known truly sub-cubic algorithms for this problem. We study the related\n                    <jats:italic>certification<\/jats:italic>\n                    task: given an instance of CFL reachability, are there small and efficiently checkable certificates for the existence and for the non-existence of a path? We show that, in both scenarios, there exist succinct certificates (\n                    <jats:italic>O<\/jats:italic>\n                    (\n                    <jats:italic>n<\/jats:italic>\n                    <jats:sup>2<\/jats:sup>\n                    ) in the size of the problem) and these certificates can be checked in subcubic (matrix multiplication) time. The certificates are based on grammar-based compression of paths (for reachability) and on invariants represented as matrix inequalities (for non-reachability). Thus, CFL reachability lies in nondeterministic and co-nondeterministic\n                    <jats:italic>subcubic<\/jats:italic>\n                    time.\n                  <\/jats:p>\n                  <jats:p>\n                    A natural question is whether faster algorithms for CFL reachability will lead to faster algorithms for combinatorial problems such as Boolean satisfiability (SAT). As a consequence of our certification results, we show that there cannot be a fine-grained reduction from SAT to CFL reachability for a conditional lower bound stronger than\n                    <jats:italic>n<\/jats:italic>\n                    <jats:sup>\u03c9<\/jats:sup>\n                    , unless the nondeterministic strong exponential time hypothesis (NSETH) fails. In a nutshell, reductions from SAT are unlikely to explain the cubic bottleneck for CFL reachability.\n                  <\/jats:p>\n                  <jats:p>Our results extend to related subcubic equivalent problems: pushdown reachability and 2NPDA recognition; as well as to all-pairs CFL reachability. For example, we describe succinct certificates for pushdown non-reachability (inductive invariants) and observe that they can be checked in matrix multiplication time. We also extract a new hardest 2NPDA language, capturing the \u201chard core\u201d of all these problems.<\/jats:p>","DOI":"10.1145\/3498702","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T12:03:12Z","timestamp":1641988992000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Subcubic certificates for CFL reachability"],"prefix":"10.1145","volume":"6","author":[{"given":"Dmitry","family":"Chistikov","sequence":"first","affiliation":[{"name":"University of Warwick, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philipp","family":"Schepper","sequence":"additional","affiliation":[{"name":"CISPA, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2015.16"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(68)91087-5"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1075382.1075387"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/22145.22192"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2016.56"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0095-8956(91)90068-U"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1137\/0210020"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00055-7"},{"key":"e_1_2_2_9_1","volume-title":"8th International Conference","volume":"150","author":"Bouajjani Ahmed","year":"1997","unstructured":"Ahmed Bouajjani , Javier Esparza , and Oded Maler . 1997 . Reachability Analysis of Pushdown Automata: Application to Model-Checking. In CONCUR \u201997: Concurrency Theory , 8th International Conference , Warsaw, Poland , July 1-4, 1997, Proceedings (Lecture Notes in Computer Science, Vol. 1243). Springer, 135\u2013 150 . Ahmed Bouajjani, Javier Esparza, and Oded Maler. 1997. Reachability Analysis of Pushdown Automata: Application to Model-Checking. In CONCUR \u201997: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings (Lecture Notes in Computer Science, Vol. 1243). Springer, 135\u2013150."},{"key":"e_1_2_2_10_1","volume-title":"Efficient Exact Paths For Dyck and semi-Dyck Labeled Path Reachability. CoRR, abs\/1802.05239","author":"Bradford Phillip G.","year":"2018","unstructured":"Phillip G. Bradford . 2018. Efficient Exact Paths For Dyck and semi-Dyck Labeled Path Reachability. CoRR, abs\/1802.05239 ( 2018 ), arxiv:1802.05239. Phillip G. Bradford. 2018. Efficient Exact Paths For Dyck and semi-Dyck Labeled Path Reachability. CoRR, abs\/1802.05239 (2018), arxiv:1802.05239."},{"key":"e_1_2_2_11_1","unstructured":"Karl Bringmann. 2018. Personal communication.  Karl Bringmann. 2018. Personal communication."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2017.36"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.151.1"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2840728.2840746"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158118"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2017.02.003"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328460"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(08)80013-2"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98654-8_23"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-48516-0_6"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(82)90401-6"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-13435-8_1"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.3390\/a10010024"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09526-8_5"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01683273"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90110-4"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(67)90369-5"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1137\/0202025"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614960"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61133-0_7"},{"key":"e_1_2_2_32_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., Boston, MA, USA. isbn:0321455363 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., Boston, MA, USA. isbn:0321455363"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1727"},{"key":"e_1_2_2_34_1","first-page":"3","article-title":"Model checking SPKI\/SDSI","volume":"12","author":"Jha Somesh","year":"2004","unstructured":"Somesh Jha and Thomas W. Reps . 2004 . Model checking SPKI\/SDSI . J. Comput. Secur. , 12 , 3 - 4 (2004), 317\u2013353. http:\/\/content.iospress.com\/articles\/journal-of-computer-security\/jcs209 Somesh Jha and Thomas W. Reps. 2004. Model checking SPKI\/SDSI. J. Comput. Secur., 12, 3-4 (2004), 317\u2013353. http:\/\/content.iospress.com\/articles\/journal-of-computer-security\/jcs209","journal-title":"J. Comput. Secur."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(93)90224-W"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-04298-5_33"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ESA.2018.56"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-8640.1994.tb00011.x"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/505241.505242"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1515\/gcc-2012-0016"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434315"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2010.09.009"},{"key":"e_1_2_2_43_1","volume-title":"Interconvertibility of a class of set constraints and context-free-language reachability. Theor. Comput. Sci., 248(1-2)","author":"Melski David","year":"2000","unstructured":"David Melski and Thomas Reps . 2000. Interconvertibility of a class of set constraints and context-free-language reachability. Theor. Comput. Sci., 248(1-2) ( 2000 ), 29\u201398. David Melski and Thomas Reps. 2000. Interconvertibility of a class of set constraints and context-free-language reachability. Theor. Comput. Sci., 248(1-2) (2000), 29\u201398."},{"key":"e_1_2_2_44_1","unstructured":"Radford Neal. 1989. The computational complexity of taxonomic inference. Unpublished manuscript. Available at http:\/\/www.cs.toronto.edu\/ radford\/ftp\/taxc.pdf  Radford Neal. 1989. The computational complexity of taxonomic inference. Unpublished manuscript. Available at http:\/\/www.cs.toronto.edu\/ radford\/ftp\/taxc.pdf"},{"key":"e_1_2_2_45_1","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1145\/263699.263712","article-title":"Proof carrying code","author":"Necula G.C.","year":"1997","unstructured":"G.C. Necula . 1997 . Proof carrying code . In POPL 97: Principles of Programming Languages. ACM , 106 \u2013 119 . G.C. Necula. 1997. Proof carrying code. In POPL 97: Principles of Programming Languages. ACM, 106\u2013119.","journal-title":"POPL 97: Principles of Programming Languages. ACM"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90269-L"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2020.105993"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90045-4"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80024-3"},{"key":"e_1_2_2_51_1","unstructured":"Wojciech Rytter. 1987. 100 exercises in the theory of automata and formal languages. http:\/\/wrap.warwick.ac.uk\/60795\/ Research report RR-99 University of Warwick Department of Computer Science available at  Wojciech Rytter. 1987. 100 exercises in the theory of automata and formal languages. http:\/\/wrap.warwick.ac.uk\/60795\/ Research report RR-99 University of Warwick Department of Computer Science available at"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.1965.11"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_33"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2019.105841"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(75)80046-8"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2213977.2214056"},{"key":"e_1_2_2_58_1","volume-title":"International Congress of Mathematicians (ICM\u201918)","author":"Williams Virginia Vassilevska","year":"2018","unstructured":"Virginia Vassilevska Williams . 2018 . On some fine-grained questions in algorithms and complexity . In International Congress of Mathematicians (ICM\u201918) . Available at https:\/\/eta.impa.br\/dl\/194.pdf Virginia Vassilevska Williams. 2018. On some fine-grained questions in algorithms and complexity. In International Congress of Mathematicians (ICM\u201918). Available at https:\/\/eta.impa.br\/dl\/194.pdf"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3186893"},{"key":"e_1_2_2_60_1","unstructured":"Mikhail Vyalyi. 2019. Personal communication.  Mikhail Vyalyi. 2019. Personal communication."},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1134\/S003294601104003X"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1134\/S0032946015040043"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_30"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/298514.298576"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498702","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498702","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T15:30:28Z","timestamp":1750174228000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498702"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":63,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498702"],"URL":"https:\/\/doi.org\/10.1145\/3498702","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"}}]}}