{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T14:29:21Z","timestamp":1754144961680,"version":"3.41.2"},"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>We develop StacKAT, a network verification language featuring loops, finite state variables, nondeterminism, and---most importantly---access to a stack with accompanying push and pop operations.  \nBy viewing the variables and stack as the (parsed) headers and (to-be-parsed) contents of a network packet, StacKAT 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 NetKAT.  \nWe develop a decision procedure for StacKAT program equivalence, based on finite automata.  \nThis decision procedure provides the theoretical basis for verifying network-wide properties and is able to provide counterexamples for inequivalent programs.  \nFinally, we provide an axiomatization of StacKAT equivalence and establish its completeness.<\/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":0,"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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6557-684X","authenticated-orcid":false,"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6068-880X","authenticated-orcid":false,"given":"Tobias","family":"Kapp\u00e9","sequence":"additional","affiliation":[{"name":"Leiden University, Leiden, Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8007-4725","authenticated-orcid":false,"given":"Dexter","family":"Kozen","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-8590-6740","authenticated-orcid":false,"given":"Lily","family":"Saada","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8616-3905","authenticated-orcid":false,"given":"Jana","family":"Wagemaker","sequence":"additional","affiliation":[{"name":"Radboud University, Nijmegen, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","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_2_2_2_1","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_2_2_3_1","doi-asserted-by":"publisher","unstructured":"Valentin M. Antimirov. 1996. Partial Derivatives of Regular Expressions and Finite Automaton Constructions. Theor. Comput. Sci. 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_2_2_4_1","volume-title":"Katra: Realtime Verification for Multilayer Networks. In NSDI. https:\/\/www.usenix.org\/conference\/nsdi22\/presentation\/beckett","author":"Beckett Ryan","year":"2022","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_2_2_5_1","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_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_2_2_7_1","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_2_2_8_1","doi-asserted-by":"publisher","unstructured":"Janusz A. Brzozowski. 1964. Derivatives of Regular Expressions. J. ACM https:\/\/doi.org\/10.1145\/321239.321249 10.1145\/321239.321249","DOI":"10.1145\/321239.321249"},{"key":"e_1_2_2_9_1","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_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3608443"},{"key":"e_1_2_2_11_1","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_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","unstructured":"Robert W. Floyd. 1963. Syntactic Analysis and Operator Precedence. J. ACM https:\/\/doi.org\/10.1145\/321172.321179 10.1145\/321172.321179","DOI":"10.1145\/321172.321179"},{"key":"e_1_2_2_14_1","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_2_2_15_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)."},{"key":"e_1_2_2_16_1","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_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3281411.3281432"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3386367.3431308"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88885-5_12"},{"key":"e_1_2_2_20_1","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_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_2_2_22_1","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_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1137\/140978818"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2017.12.001"},{"key":"e_1_2_2_25_1","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_2_2_26_1","doi-asserted-by":"publisher","unstructured":"Robert McNaughton. 1967. Parenthesis Grammars. J. ACM https:\/\/doi.org\/10.1145\/321406.321411 10.1145\/321406.321411","DOI":"10.1145\/321406.321411"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SWAT.1972.29"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656454"},{"key":"e_1_2_2_29_1","unstructured":"Francesco Pontiggia Ezio Bartocci and Michele Chiari. 2025. Model Checking Probabilistic Operator Precedence Automata. arxiv:2404.03515. arxiv:2404.03515"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","unstructured":"Damien Pous Jurriaan Rot and Jana Wagemaker. 2024. On Tools for Completeness of Kleene Algebra with Hypotheses. LMCS 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_2_2_31_1","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_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"e_1_2_2_33_1","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_2_2_34_1","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_2_2_35_1","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_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2005.02.009"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","unstructured":"Shmuel Sagiv Thomas W. Reps and Susan Horwitz. 1996. Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation. Theor. Comput. Sci. https:\/\/doi.org\/10.1016\/0304-3975(96)00072-2 10.1016\/0304-3975(96)00072-2","DOI":"10.1016\/0304-3975(96)00072-2"},{"key":"e_1_2_2_38_1","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_2_2_39_1","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_2_2_40_1","doi-asserted-by":"publisher","unstructured":"G\u00e9raud S\u00e9nizergues. 2002. L(A)=L(B)? A simplified decidability proof. Theor. Comput. Sci. 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_2_2_41_1","unstructured":"Alexandra Silva. 2010. Kleene Coalgebra. Ph. D. Dissertation. Radboud Universiteit Nijmegen."},{"key":"e_1_2_2_42_1","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_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1024853.1024855"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(75)80005-5"},{"key":"e_1_2_2_45_1","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":[[2025,7,16]],"date-time":"2025-07-16T06:05:38Z","timestamp":1752645938000},"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":[{"type":"electronic","value":"2475-1421"}],"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"}}]}}