{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:43Z","timestamp":1780994683016,"version":"3.54.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"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":["N68335-22-C-0411"],"award-info":[{"award-number":["N68335-22-C-0411"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["W912CG23C0032"],"award-info":[{"award-number":["W912CG23C0032"]}],"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":[[2024,6,20]]},"abstract":"<jats:p>We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for building efficient and scalable verification tools. We present KATch, an implementation of these ideas in Scala, featuring an extended set of NetKAT operators that are useful for expressing network-wide specifications, and a verification engine that constructs a bisimulation or generates a counter-example showing that none exists. We evaluate the performance of our implementation on real-world and synthetic benchmarks, verifying properties such as reachability and slice isolation, typically returning a result in well under a second, which is orders of magnitude faster than previous approaches. Our advancements underscore NetKAT\u2019s potential as a practical, declarative language for network specification and verification.<\/jats:p>","DOI":"10.1145\/3656454","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1905-1928","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["KATch: A Fast Symbolic Verifier for NetKAT"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-9512-565X","authenticated-orcid":false,"given":"Mark","family":"Moeller","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1976-3182","authenticated-orcid":false,"given":"Jules","family":"Jacobs","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2809-6047","authenticated-orcid":false,"given":"Olivier Savary","family":"Belanger","sequence":"additional","affiliation":[{"name":"Galois, Portland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2314-0287","authenticated-orcid":false,"given":"David","family":"Darais","sequence":"additional","affiliation":[{"name":"Galois, Portland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9350-3041","authenticated-orcid":false,"given":"Cole","family":"Schlesinger","sequence":"additional","affiliation":[{"name":"Galois, Portland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8625-5490","authenticated-orcid":false,"given":"Steffen","family":"Smolka","sequence":"additional","affiliation":[{"name":"Google, Mountain View, 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-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_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_1_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00182-4"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","unstructured":"Michael Barnett Bor-Yuh Evan Chang Robert DeLine Bart Jacobs and K. Rustan M. Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO. https:\/\/doi.org\/10.1007\/11804192_17 10.1007\/11804192_17","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2017. A General Approach to Network Configuration Verification. In SIGCOMM. https:\/\/doi.org\/10.1145\/3098822.3098834 10.1145\/3098822.3098834","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2018. Control Plane Compression. In SIGCOMM. https:\/\/doi.org\/10.1145\/3230543.3230583 10.1145\/3230543.3230583","DOI":"10.1145\/3230543.3230583"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","unstructured":"Ryan Beckett Aarti Gupta Ratul Mahajan and David Walker. 2020. Abstract Interpretation of Distributed Network Control Planes. In POPL. https:\/\/doi.org\/10.1145\/3371110 10.1145\/3371110","DOI":"10.1145\/3371110"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","unstructured":"Ryan Beckett Ratul Mahajan Todd Millstein Jitendra Padhye and David Walker. 2016. Don\u2019t Mind the Gap: Bridging Network-Wide Objectives and Device-Level Configurations. In SIGCOMM. https:\/\/doi.org\/10.1145\/2934872.2934909 10.1145\/2934872.2934909","DOI":"10.1145\/2934872.2934909"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","unstructured":"Filippo Bonchi and Damien Pous. 2013. Checking NFA Equivalence with Bisimulations up to Congruence. In POPL. https:\/\/doi.org\/10.1145\/2429069.2429124 10.1145\/2429069.2429124","DOI":"10.1145\/2429069.2429124"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","unstructured":"Matt Brown Ari Fogel Daniel Halperin Victor Heorhiadi Ratul Mahajan and Todd D. Millstein. 2023. Lessons from the evolution of the Batfish configuration analysis tool. In SIGCOMM. https:\/\/doi.org\/10.1145\/3603269.3604866 10.1145\/3603269.3604866","DOI":"10.1145\/3603269.3604866"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_3_1_14_2","unstructured":"Janusz A. Brzozowski. 1962. Canonical regular expressions and minimal state graphs for definite events. In Proceedings of the Symposium of Mathematical Theory of Automata."},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","unstructured":"Jerry R. Burch Edmund M. Clarke Kenneth L. McMillan David L. Dill and L. J. Hwang. 1990. Symbolic Model Checking: 10^20 States and Beyond. In LICS. https:\/\/doi.org\/10.1109\/LICS.1990.113767 10.1109\/LICS.1990.113767","DOI":"10.1109\/LICS.1990.113767"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_8"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","unstructured":"Loris D\u2019Antoni and Margus Veanes. 2014. Minimization of Symbolic Automata. In POPL. https:\/\/doi.org\/10.1145\/2535838.2535849 10.1145\/2535838.2535849","DOI":"10.1145\/2535838.2535849"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Loris D\u2019Antoni and Margus Veanes. 2017. Forward Bisimulations for Nondeterministic Symbolic Finite Automata. In TACAS. https:\/\/doi.org\/10.1007\/978-3-662-54577-5_30 10.1007\/978-3-662-54577-5_30","DOI":"10.1007\/978-3-662-54577-5_30"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Ryan Doenges Tobias Kapp\u00e9 John Sarracino Nate Foster and Greg Morrisett. 2022. Leapfrog: Certified Equivalence for Protocol Parsers. In PLDI. https:\/\/doi.org\/10.1145\/3519939.3523715 10.1145\/3519939.3523715","DOI":"10.1145\/3519939.3523715"},{"key":"e_1_3_1_20_2","unstructured":"Ari Fogel Stanley Fung Luis Pedrosa Meg Walraed-Sullivan Ramesh Govindan Ratul Mahajan and Todd Millstein. 2015. A General Approach to Network Configuration Analysis. In NSDI."},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Nate Foster Rob Harrison Michael J. Freedman Christopher Monsanto Jennifer Rexford Alec Story and David Walker. 2011. Frenetic: A Network Programming Language. In ICFP. https:\/\/doi.org\/10.1145\/2034773.2034812 10.1145\/2034773.2034812","DOI":"10.1145\/2034773.2034812"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Nate Foster Dexter Kozen Konstantinos Mamouras Mark Reitblatt and Alexandra Silva. 2016. Probabilistic NetKAT. In ESOP. https:\/\/doi.org\/10.1007\/978-3-662-49498-1_12 10.1007\/978-3-662-49498-1_12","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"e_1_3_1_23_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_1_24_2","doi-asserted-by":"publisher","unstructured":"Michael Greenberg Ryan Beckett and Eric Campbell. 2022. Kleene Algebra Modulo Theories: A Framework for Concrete KATs. In PLDI. https:\/\/doi.org\/10.1145\/3519939.3523722 10.1145\/3519939.3523722","DOI":"10.1145\/3519939.3523722"},{"key":"e_1_3_1_25_2","unstructured":"Pieter Hooimeijer Benjamin Livshits David Molnar Prateek Saxena and Margus Veanes. 2011. Fast and Precise Sanitizer Analysis with BEK. In USENIX Conference on Security."},{"key":"e_1_3_1_26_2","unstructured":"John E. Hopcroft and Richard M. Karp. 1971. A Linear Algorithm for Testing Equivalence of Finite Automata."},{"key":"e_1_3_1_27_2","unstructured":"Peyman Kazemian George Varghese and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In NSDI."},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2377677.2377766"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2011.111002"},{"key":"e_1_3_1_30_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_1_31_2","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1959.tb01585.x"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","unstructured":"K. Rustan M. Leino and Valentin W\u00fcstholz. 2014. The Dafny Integrated Development Environment. In F-IDE. https:\/\/doi.org\/10.4204\/EPTCS.149.2 10.4204\/EPTCS.149.2","DOI":"10.4204\/EPTCS.149.2"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2043164.2018470"},{"key":"e_1_3_1_34_2","doi-asserted-by":"crossref","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. arXiv:2404.04760 [cs.PL] https:\/\/arxiv.org\/pdf\/2404.04760.pdf","DOI":"10.1145\/3656454"},{"key":"e_1_3_1_35_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. https:\/\/doi.org\/10.5281\/zenodo.10961123 10.5281\/zenodo.10961123","DOI":"10.5281\/zenodo.10961123"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1515\/9781400882618-006"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","unstructured":"Damien Pous. 2015. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. In POPL. https:\/\/doi.org\/10.1145\/2775051.2677007 10.1145\/2775051.2677007","DOI":"10.1145\/2775051.2677007"},{"key":"e_1_3_1_38_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_1_39_2","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Nate Foster Justin Hsu Tobias Kapp\u00e9 Dexter Kozen and Alexandra Silva. 2019. Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time. In POPL. https:\/\/doi.org\/10.1145\/3371129 10.1145\/3371129","DOI":"10.1145\/3371129"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Praveen Kumar Nate Foster Justin Hsu Dexter Kozen and Alexandra Silva. 2019. Scalable Verification of Probabilistic Networks. In PLDI. https:\/\/doi.org\/10.1145\/3314221.3314639 10.1145\/3314221.3314639","DOI":"10.1145\/3314221.3314639"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Praveen Kumar Nate Foster Dexter Kozen and Alexandra Silva. 2017. Cantor Meets Scott: Semantic Foundations for Probabilistic Networks. In POPL. https:\/\/doi.org\/10.1145\/3093333.3009843 10.1145\/3093333.3009843","DOI":"10.1145\/3093333.3009843"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Alan Tang Ryan Beckett Steven Benaloh Karthick Jayaraman Tejas Patil Todd D. Millstein and George Varghese. 2023. Lightyear: Using Modularity to Scale BGP Control Plane Verification. In SIGCOMM. https:\/\/doi.org\/10.1145\/3603269.3604842 10.1145\/3603269.3604842","DOI":"10.1145\/3603269.3604842"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","unstructured":"Timothy Alberdingk Thijm Ryan Beckett Aarti Gupta and David Walker. 2023. Modular Control Plane Verification via Temporal Invariants. In PLDI. https:\/\/doi.org\/10.1145\/3591222 10.1145\/3591222","DOI":"10.1145\/3591222"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","unstructured":"Emina Torlak and Rastislav Bod\u00edk. 2013. Growing Solver-aided Languages with Rosette. In Onward! (SPLASH). https:\/\/doi.org\/10.1145\/2509578.2509586 10.1145\/2509578.2509586","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_1_45_2","unstructured":"Moshe Y. Vardi and Pierre Wolper. 1986. An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). In LICS."},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","unstructured":"Geoffry G. Xie Jibin Zhan David A. Maltz Hui Zhang Albert Greenberg Gisli Hjalmtysson and Jennifer Rexford. 2005. On Static Reachability Analysis of IP Networks. In INFOCOMM. https:\/\/doi.org\/10.1109\/INFCOM.2005.1498492 10.1109\/INFCOM.2005.1498492","DOI":"10.1109\/INFCOM.2005.1498492"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2015.2398197"},{"key":"e_1_3_1_48_2","unstructured":"Peng Zhang Xu Liu Hongkun Yang Ning Kang Zhengchang Gu and Hao Li. 2020. APKeep: Realtime Verification for Real Networks. In NSDI."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656454","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656454","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:42:01Z","timestamp":1751661721000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656454"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":47,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656454"],"URL":"https:\/\/doi.org\/10.1145\/3656454","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}