{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:04:45Z","timestamp":1784199885205,"version":"3.55.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    We develop StacKAT, a network verification language featuring loops, finite state variables, nondeterminism, and\u2014most importantly\u2014access to a stack with accompanying push and pop operations. By viewing the variables and stack as the (parsed) headers and (to-be-parsed) contents of a network packet,\n                    <jats:monospace>StacKAT<\/jats:monospace>\n                    can express a wide range of network behaviors including parsing, source routing, and telemetry. These behaviors are difficult or impossible to model using existing languages like\n                    <jats:monospace>NetKAT<\/jats:monospace>\n                    . We develop a decision procedure for\n                    <jats:monospace>StacKAT<\/jats:monospace>\n                    program equivalence, based on finite automata. This decision procedure provides the theoretical basis for verifying network-wide properties and is able to provide counterexamples for inequivalent programs. Finally, we provide an axiomatization of\n                    <jats:monospace>StacKAT<\/jats:monospace>\n                    equivalence and establish its completeness.\n                  <\/jats:p>","DOI":"10.1145\/3729257","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"277-300","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["StacKAT: Infinite State Network Verification"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1976-3182","authenticated-orcid":false,"given":"Jules","family":"Jacobs","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6557-684X","authenticated-orcid":false,"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6068-880X","authenticated-orcid":false,"given":"Tobias","family":"Kapp\u00e9","sequence":"additional","affiliation":[{"name":"Leiden University, Leiden, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8007-4725","authenticated-orcid":false,"given":"Dexter","family":"Kozen","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-8590-6740","authenticated-orcid":false,"given":"Lily","family":"Saada","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8616-3905","authenticated-orcid":false,"given":"Jana","family":"Wagemaker","sequence":"additional","affiliation":[{"name":"Radboud University, Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Rajeev Alur and P. Madhusudan. 2004. Visibly pushdown languages. In STOC. https:\/\/doi.org\/10.1145\/1007352.1007390 10.1145\/1007352.1007390","DOI":"10.1145\/1007352.1007390"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Carolyn Jane Anderson Nate Foster Arjun Guha Jean-Baptiste Jeannin Dexter Kozen Cole Schlesinger and David Walker. 2014. NetKAT: Semantic Foundations for Networks. In POPL. https:\/\/doi.org\/10.1145\/2535838.2535862 10.1145\/2535838.2535862","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Valentin M. Antimirov. 1996. Partial Derivatives of Regular Expressions and Finite Automaton Constructions. Theor. Comput. Sci. (1996). https:\/\/doi.org\/10.1016\/0304-3975(95)00182-4 10.1016\/0304-3975(95)00182-4","DOI":"10.1016\/0304-3975(95)00182-4"},{"key":"e_1_3_2_5_2","unstructured":"Ryan Beckett and Aarti Gupta. 2022. Katra: Realtime Verification for Multilayer Networks. In NSDI. https:\/\/www.usenix.org\/conference\/nsdi22\/presentation\/beckett"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Jean Berstel and Luc Boasson. 2002. Balanced Grammars and Their Languages. In Formal and Natural Computing - Essays Dedicated to Grzegorz Rozenberg. https:\/\/doi.org\/10.1007\/3-540-45711-9_1 10.1007\/3-540-45711-9_1","DOI":"10.1007\/3-540-45711-9_1"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Pat Bosshart Dan Daly Glen Gibb Martin Izzard Nick McKeown Jennifer Rexford Cole Schlesinger Dan Talayco Amin Vahdat George Varghese and David Walker. 2014. P4: Programming Protocol-Independent Packet Processors. SIGCOMM (07 2014). https:\/\/doi.org\/10.1145\/2656877.2656890 10.1145\/2656877.2656890","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani Javier Esparza and Oded Maler. 1997. Reachability Analysis of Pushdown Automata: Application to Model-Checking. In CONCUR. https:\/\/doi.org\/10.1007\/3-540-63141-0_10 10.1007\/3-540-63141-0_10","DOI":"10.1007\/3-540-63141-0_10"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Janusz A. Brzozowski. 1964. Derivatives of Regular Expressions. J. ACM (1964). https:\/\/doi.org\/10.1145\/321239.321249 10.1145\/321239.321249","DOI":"10.1145\/321239.321249"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"P. Buckheister and Georg Zetzsche. 2013. Semilinearity and Context-Freeness of Languages Accepted by Valence Automata. In MFCS. https:\/\/doi.org\/10.1007\/978-3-642-40313-2_22 10.1007\/978-3-642-40313-2_22","DOI":"10.1007\/978-3-642-40313-2_22"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3608443"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Amina Doumane Denis Kuperberg Damien Pous and C\u00e9cilia Pradic. 2019. Kleene Algebra with Hypotheses. In FOSSACS. https:\/\/doi.org\/10.1007\/978-3-030-17127-8_12 10.1007\/978-3-030-17127-8_12","DOI":"10.1007\/978-3-030-17127-8_12"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Alain Finkel Bernard Willems and Pierre Wolper. 1997. A direct symbolic approach to model checking pushdown systems. In Workshop on Verification of Infinite State Systems. https:\/\/doi.org\/10.1016\/S1571-0661(05)80426-8 10.1016\/S1571-0661(05)80426-8","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Robert W. Floyd. 1963. Syntactic Analysis and Operator Precedence. J. ACM (1963). https:\/\/doi.org\/10.1145\/321172.321179 10.1145\/321172.321179","DOI":"10.1145\/321172.321179"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Nate Foster Dexter Kozen Mae Milano Alexandra Silva and Laure Thompson. 2015. A Coalgebraic Decision Procedure for NetKAT. In POPL. https:\/\/doi.org\/10.1145\/2676726.2677011 10.1145\/2676726.2677011","DOI":"10.1145\/2676726.2677011"},{"key":"e_1_3_2_16_2","unstructured":"John E. Hopcroft Rajeev Motwani and Jeffrey D. Ullman. 2006. Introduction to Automata Theory Languages and Computation (3rd Edition)."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Susan Horwitz Thomas W. Reps and Shmuel Sagiv. 1995. Demand Interprocedural Dataflow Analysis. In SIGSOFT. https:\/\/doi.org\/10.1145\/222124.222146 10.1145\/222124.222146","DOI":"10.1145\/222124.222146"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Jesper Stenbjerg Jensen Troels Beck Kr\u00f8gh Jonas S and Madsen Stefan Schmid Jir\u00ed Srba and Marc Tom Thorgersen. 2018. P-Rex: fast verification of MPLS networks with multiple link failures. In CoNEXT. https:\/\/doi.org\/10.1145\/3281411.3281432 10.1145\/3281411.3281432","DOI":"10.1145\/3281411.3281432"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Peter Gj\u00f8l Jensen Dan Kristiansen Stefan Schmid Morten Konggaard Schou Bernhard Clemens Schrenk and Jir\u00ed Srba. 2020. AalWiNes: a fast and quantitative what-if analysis tool for MPLS networks. In CoNEXT. https:\/\/doi.org\/10.1145\/3386367.3431308 10.1145\/3386367.3431308","DOI":"10.1145\/3386367.3431308"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Peter Gj\u00f8l Jensen Stefan Schmid Morten Konggaard Schou Jir\u00ed Srba Juan Vanerio and Ingo van Duijn. 2021. Faster Pushdown Reachability Analysis with Applications in Network Verification. In ATVA. https:\/\/doi.org\/10.1007\/978-3-030-88885-5_12 10.1007\/978-3-030-88885-5_12","DOI":"10.1007\/978-3-030-88885-5_12"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Adam Husted Kjelstr\u00f8m and Andreas Pavlogiannis. 2022. The decidability and complexity of interleaved bidirected Dyck reachability. In POPL. https:\/\/doi.org\/10.1145\/3498673 10.1145\/3498673","DOI":"10.1145\/3498673"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 1994. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Inf. Comput. (1994). https:\/\/doi.org\/10.1006\/inco.1994.1037 10.1006\/inco.1994.1037","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 1996. Kleene algebra with tests and commutativity conditions. In TACAS. https:\/\/doi.org\/10.1007\/3-540-61042-1_35 10.1007\/3-540-61042-1_35","DOI":"10.1007\/3-540-61042-1_35"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1137\/140978818"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2017.12.001"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Vincent Mathieu and Jules Desharnais. 2005. Verification of Pushdown Systems Using Omega Algebra with Domain. In RelMICS\/AKA. https:\/\/doi.org\/10.1007\/11734673_15 10.1007\/11734673_15","DOI":"10.1007\/11734673_15"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Robert McNaughton. 1967. Parenthesis Grammars. J. ACM (1967). https:\/\/doi.org\/10.1145\/321406.321411 10.1145\/321406.321411","DOI":"10.1145\/321406.321411"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Albert R. Meyer and Larry J. Stockmeyer. 1972. The Equivalence Problem for Regular Expressions with Squaring Requires Exponential Space. In SWAT. https:\/\/doi.org\/10.1109\/SWAT.1972.29 10.1109\/SWAT.1972.29","DOI":"10.1109\/SWAT.1972.29"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Mark Moeller Jules Jacobs Olivier Savary Belanger David Darais Cole Schlesinger Steffen Smolka Nate Foster and Alexandra Silva. 2024. KATch: A Fast Symbolic Verifier for NetKAT. In PLDI. https:\/\/doi.org\/10.1145\/3656454 10.1145\/3656454","DOI":"10.1145\/3656454"},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","unstructured":"Francesco Pontiggia Ezio Bartocci and Michele Chiari. 2025. Model Checking Probabilistic Operator Precedence Automata. arXiv:2404.03515 https:\/\/arxiv.org\/abs\/2404.03515","DOI":"10.1145\/3822593"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Damien Pous Jurriaan Rot and Jana Wagemaker. 2024. On Tools for Completeness of Kleene Algebra with Hypotheses. LMCS (2024). https:\/\/doi.org\/10.46298\/LMCS-20(2:8)2024 10.46298\/LMCS-20(2:8)2024","DOI":"10.46298\/LMCS-20(2:8)2024"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Jakob Rehof and Manuel F\u00e4hndrich. 2001. Type-base flow analysis: from polymorphic subtyping to CFL-reachability. In POPL. https:\/\/doi.org\/10.1145\/360204.360208 10.1145\/360204.360208","DOI":"10.1145\/360204.360208"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Thomas W. Reps Susan Horwitz and Shmuel Sagiv. 1995. Precise Interprocedural Dataflow Analysis via Graph Reachability. In POPL. https:\/\/doi.org\/10.1145\/199448.199462 10.1145\/199448.199462","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Thomas W. Reps Susan Horwitz Shmuel Sagiv and Genevieve Rosay. 1994. Speeding up Slicing. In SIGSOFT. https:\/\/doi.org\/10.1145\/193173.195287 10.1145\/193173.195287","DOI":"10.1145\/193173.195287"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Thomas W. Reps Stefan Schwoon and Somesh Jha. 2003. Weighted Pushdown Systems and Their Application to Interprocedural Dataflow Analysis. In SAS. https:\/\/doi.org\/10.1007\/3-540-44898-5_11 10.1007\/3-540-44898-5_11","DOI":"10.1007\/3-540-44898-5_11"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Thomas W. Reps Stefan Schwoon Somesh Jha and David Melski. 2005. Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program. (2005). https:\/\/doi.org\/10.1016\/J.SCICO.2005.02.009 10.1016\/J.SCICO.2005.02.009","DOI":"10.1016\/J.SCICO.2005.02.009"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00072-2"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"G\u00e9raud S\u00e9nizergues. 1997. The Equivalence Problem for Deterministic Pushdown Automata is Decidable. In ICALP. https:\/\/doi.org\/10.1007\/3-540-63165-8_221 10.1007\/3-540-63165-8_221","DOI":"10.1007\/3-540-63165-8_221"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"G\u00e9raud S\u00e9nizergues. 2002. L(A) = L(B)? Decidability Results from Complete Formal Systems. In ICALP. https:\/\/doi.org\/10.1007\/3-540-45465-9_4 10.1007\/3-540-45465-9_4","DOI":"10.1007\/3-540-45465-9_4"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"G\u00e9raud S\u00e9nizergues. 2002. L(A)=L(B)? A simplified decidability proof. Theor. Comput. Sci. (2002). https:\/\/doi.org\/10.1016\/S0304-3975(02)00027-0 10.1016\/S0304-3975(02)00027-0","DOI":"10.1016\/S0304-3975(02)00027-0"},{"key":"e_1_3_2_42_2","volume-title":"Kleene Coalgebra","author":"Silva Alexandra","year":"2010","unstructured":"Alexandra Silva. 2010. Kleene Coalgebra. Ph. D. Dissertation. Radboud Universiteit Nijmegen."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Spiridon Eliopoulos Nate Foster and Arjun Guha. 2015. A Fast Compiler for NetKAT. In ICFP. https:\/\/doi.org\/10.1145\/2784731.2784761 10.1145\/2784731.2784761","DOI":"10.1145\/2784731.2784761"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Carl A. Sunshine. 1977. Source routing in computer networks. Comput. Commun. Rev. (1977). https:\/\/doi.org\/10.1145\/1024853.1024855 10.1145\/1024853.1024855","DOI":"10.1145\/1024853.1024855"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","unstructured":"Leslie G. Valiant and Michael S. Paterson. 1975. Deterministic one-counter automata. J. Comput. Syst. Sci. (1975). https:\/\/doi.org\/10.1016\/S0022-0000(75)80005-5 10.1016\/S0022-0000(75)80005-5","DOI":"10.1016\/S0022-0000(75)80005-5"},{"key":"e_1_3_2_46_2","unstructured":"Peng Zhang Xu Liu Hongkun Yang Ning Kang Zhengchang Gu and Hao Li. 2020. APKeep: Realtime Verification for Real Networks. In NSDI. https:\/\/www.usenix.org\/conference\/nsdi20\/presentation\/zhang-peng"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729257","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729257","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:05:19Z","timestamp":1784196319000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729257"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":45,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729257"],"URL":"https:\/\/doi.org\/10.1145\/3729257","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}