{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:12:27Z","timestamp":1784837547699,"version":"3.55.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["DGE \u2013 2139899"],"award-info":[{"award-number":["DGE \u2013 2139899"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004836","name":"Danmarks Frie Forskningsfond","doi-asserted-by":"publisher","award":["AuRoRa"],"award-info":[{"award-number":["AuRoRa"]}],"id":[{"id":"10.13039\/501100004836","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR001125CE018"],"award-info":[{"award-number":["HR001125CE018"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101002697"],"award-info":[{"award-number":["101002697"]}],"id":[{"id":"10.13039\/501100000781","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":[[2026,6,8]]},"abstract":"<jats:p>We introduce weighted NetKAT, a domain-specific language for modeling and verifying quantitative network properties. The language is parametric on a semiring, enabling the treatment of a wide range of quantities in a uniform way. We provide a denotational semantics and an equivalent operational semantics, the latter based on a novel model of weighted NetKAT automata (WNKA) capturing the stateful behavior of our language. With WNKA, we obtain a class of generic decision procedures for reasoning about quantitative safety and reachability in a fully automatic way, even in the presence of possibly unbounded iteration. We demonstrate the applicability of our framework in a case study using Internet2's Abilene network as the underlying topology.<\/jats:p>","DOI":"10.1145\/3808318","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"1788-1811","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Weighted NetKAT: A Programming Language for Quantitative Network Verification"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-5515-6099","authenticated-orcid":false,"given":"Emmanuel","family":"Su\u00e1rez Acevedo","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6942-0228","authenticated-orcid":false,"given":"Tiago","family":"Ferreira","sequence":"additional","affiliation":[{"name":"University College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4702-2876","authenticated-orcid":false,"given":"Oliver","family":"B\u00f8ving","sequence":"additional","affiliation":[{"name":"Technical University of Denmark, Kongens Lyngby, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6557-684X","authenticated-orcid":false,"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"},{"name":"Jane Street, New York, 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":[[2026,6,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544220"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104651"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535862"},{"key":"e_1_2_1_4_1","unstructured":"The NetKAT authors. 2025. NetKAT. https:\/\/github.com\/google\/netkat"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527310"},{"key":"e_1_2_1_6_1","volume-title":"Noncommutative Rational Series with Applications (Encyclopedia of Mathematics and its Applications","author":"Berstel Jean","unstructured":"Jean Berstel and Christophe Reutenauer. 2010. Noncommutative Rational Series with Applications (Encyclopedia of Mathematics and its Applications, Vol. 137). Cambridge University Press, Cambridge, UK. isbn:978-0-521-19022-0"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-78034-9_10"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2490818"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2677011"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1265530.1265535"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1080091.1080094"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2619239.2626300"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2534169.2486019"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342094"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80027-9"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/646246.684713"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(94)90090-6"},{"key":"e_1_2_1_21_1","unstructured":"Kim G. Larsen Stefan Schmid and Bingtian Xue. 2016. WNetKAT: A Weighted SDN Programming and Verification Language. arxiv:1608.08483. arxiv:1608.08483"},{"key":"e_1_2_1_22_1","volume-title":"Network calculus: a theory of deterministic queuing systems for the Internet","author":"Le Boudec Jean-Yves","unstructured":"Jean-Yves Le Boudec and Patrick Thiran. 2001. Network calculus: a theory of deterministic queuing systems for the Internet. Springer-Verlag, Berlin, Heidelberg. isbn:354042184X"},{"key":"e_1_2_1_23_1","unstructured":"Mark Moeller. [n. d.]. Galois Internship Round 2: A Second Summer Intern Experience. https:\/\/web.archive.org\/web\/20251010101506\/https:\/\/www.galois.com\/articles\/galois-internship-round-2-a-second-summer-intern-experience Accessed: 2025-11-13"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729295"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656454"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01492-5_6"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Igor Sedl\u00e1r. 2024. Completeness of\u00a0Finitely Weighted Kleene Algebra with\u00a0Tests. In Logic Language Information and Computation George Metcalfe Thomas Studer and Ruy de Queiroz (Eds.). Springer Nature Switzerland Cham. 210\u2013224. isbn:978-3-031-62687-6","DOI":"10.1007\/978-3-031-62687-6_14"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL57333.2023.00031"},{"key":"e_1_2_1_29_1","unstructured":"Avaljot Singh. 2021. Cost InterNetKAT: Basics of Algebraic Network Routing. Ph. D. Dissertation. INDIAN INSTITUTE OF TECHNOLOGY DELHI."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371129"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009843"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314639"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2005.857111"},{"key":"e_1_2_1_34_1","unstructured":"Emmanuel Su\u00e1rez Acevedo Tiago Ferreira Kevin Batz Oliver B\u00f8ving Nate Foster and Alexandra Silva. 2026. Weighted NetKAT: A Programming Language For Quantitative Network Verification. arxiv:2604.13987. arxiv:2604.13987"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2025.172"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.7298\/Y5X5-JR17"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808318","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808318","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T20:04:42Z","timestamp":1780949082000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808318"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":36,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808318"],"URL":"https:\/\/doi.org\/10.1145\/3808318","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}