pith. machine review for the scientific record. sign in

arxiv: 2604.13987 · v1 · submitted 2026-04-15 · 💻 cs.PL

Recognition: unknown

Weighted NetKAT: A Programming Language For Quantitative Network Verification

Alexandra Silva, Emmanuel Su\'arez Acevedo, Kevin Batz, Nate Foster, Oliver B{\o}ving, Tiago Ferreira

Pith reviewed 2026-05-10 11:54 UTC · model grok-4.3

classification 💻 cs.PL
keywords weighted NetKATquantitative network verificationsemiring semanticsweighted automatasafety propertiesreachabilitynetwork programming languagesdenotational semantics
0
0 comments X

The pith

Weighted NetKAT provides a semiring-based language and automata for automatically verifying quantitative network properties.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper introduces weighted NetKAT, a domain-specific language that models networks while incorporating quantitative measures such as costs or probabilities through a single semiring parameter. It supplies both a denotational semantics and an equivalent operational semantics realized by weighted NetKAT automata that track stateful weighted transitions. These automata yield generic, fully automatic decision procedures for quantitative safety and reachability questions, including programs that contain unbounded iteration. The framework is applied to the Abilene network topology to illustrate its use on a concrete, real-world routing structure.

Core claim

We introduce weighted NetKAT, a domain-specific language parametric on a semiring for modeling and verifying quantitative network properties. We provide a denotational semantics and an equivalent operational semantics, the latter based on a novel model of weighted NetKAT automata 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.

What carries the argument

Weighted NetKAT automata (WNKA), which model stateful weighted network behavior and directly support automatic decision procedures for quantitative properties.

Load-bearing premise

The operational semantics defined by weighted NetKAT automata is equivalent to the denotational semantics, so the derived decision procedures correctly decide the quantitative properties.

What would settle it

A concrete network program with unbounded iteration together with a safety or reachability property whose true quantitative value computed from the denotational semantics differs from the value returned by the WNKA decision procedure.

Figures

Figures reproduced from arXiv: 2604.13987 by Alexandra Silva, Emmanuel Su\'arez Acevedo, Kevin Batz, Nate Foster, Oliver B{\o}ving, Tiago Ferreira.

Figure 1
Figure 1. Figure 1: Sample network and its encoding in wNetKAT. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Sample network with links now weighted by [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Instances of wNetKAT: examples of semirings [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Quantitative verification pipeline of wNetKAT instantiated with a semiring [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Definition of (𝜔-continuous) semirings. Semirings offer an algebraic basis to formalize weights and relevant operations, whereas 𝜔-continuity captures the existence of adequate countable sums, essential for the semantics of iteration. All details are provided in Section A . (accumulating an unbounded latency). Our decision procedure identifies this updated network as violating the safety property and provi… view at source ↗
Figure 6
Figure 6. Figure 6: Syntax and Semantics of S-wNetKAT, where S = (𝑆, +, ·, 0, 1) is an 𝜔-continuous semiring. We assume that the operators bind stronger in the order: ¬, ∧ , ∨ , ;, ⊙, ⊕. 3.1 Syntax The syntax of wNetKAT is shown in [PITH_FULL_IMAGE:figures/full_fig_p008_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Reduced wNetKAT Syntax. 4 Language Model In this section, we define the language model of wNetKAT, in which each policy 𝑝 is assigned a weighting of guarded strings, generalizing NetKAT’s languages of guarded strings. 4.1 Reduced Syntax First, we restrict all wNetKAT policies to a reduced syntax, see [PITH_FULL_IMAGE:figures/full_fig_p011_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Language Model. or equivalently, functions 𝐺 : Pol → 2 GS so we are generalizing the Boolean semiring underlying sets to an arbitrary 𝜔-continuous semiring (note that 2 GS  𝒲2 (GS)). Definition 2 (Language Model). Let 𝑝 be a wNetKAT policy. We define the weighted language 𝐺(𝑝) of 𝑝 as the weighting 𝐺(𝑝): 𝒲S (GS) given by the table in [PITH_FULL_IMAGE:figures/full_fig_p012_8.png] view at source ↗
Figure 10
Figure 10. Figure 10: Topology from Abilene network with links between nodes weighted by [PITH_FULL_IMAGE:figures/full_fig_p019_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Approximants of policies in wNetKAT. Recall that [PITH_FULL_IMAGE:figures/full_fig_p030_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Reduction map for wNetKAT policies to reduced wNetKAT policies. [PITH_FULL_IMAGE:figures/full_fig_p047_12.png] view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 4 minor

Summary. The paper introduces Weighted NetKAT, a semiring-parametric domain-specific language for modeling and verifying quantitative network properties. It defines a denotational semantics and proves equivalence to an operational semantics realized by a novel model of weighted NetKAT automata (WNKA) that captures stateful behavior. This equivalence is used to derive generic, fully automatic decision procedures for quantitative safety and reachability properties, including in the presence of unbounded iteration. The framework is demonstrated via a case study on Internet2's Abilene network topology.

Significance. If the claimed equivalence and decision procedures hold, this work meaningfully extends the NetKAT framework from qualitative to quantitative network verification in a uniform, semiring-parametric manner. The automata-based operational model and automatic procedures for safety/reachability (even with iteration) represent a substantive technical advance with clear applicability to practical network analysis. The Abilene case study provides concrete grounding.

minor comments (4)
  1. §3 (Denotational Semantics): The semiring-parametric definitions are clear at a high level, but the interaction between the semiring operations and the Kleene star (iteration) could be illustrated with a small concrete example to aid readability.
  2. §5 (Decision Procedures): The description of the generic procedures derived from WNKA would benefit from an explicit complexity bound or termination argument for the unbounded-iteration case, even if it is polynomial in the automaton size.
  3. Figure 2 (Abilene topology): The diagram is helpful but the edge weights used in the case study should be stated explicitly in the caption or accompanying text rather than only in the prose.
  4. Related Work section: The comparison to prior quantitative extensions of NetKAT or other automata-based network languages could be expanded by one paragraph to better situate the novelty of WNKA.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of Weighted NetKAT, including recognition of the semiring-parametric extension, the WNKA model, the decision procedures for quantitative safety and reachability (even with iteration), and the Abilene case study. We note the recommendation for minor revision.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper defines a semiring-parametric DSL, supplies a denotational semantics, and proves equivalence to an operational semantics realized by the newly introduced WNKA model. The generic decision procedures for quantitative safety and reachability follow directly from that equivalence proof and the automata construction; they are not obtained by fitting parameters to the target properties or by renaming prior results. The Abilene case study supplies an independent, externally grounded validation. No self-definitional equations, fitted-input predictions, or load-bearing self-citations appear in the core chain. The framework is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on standard properties of semirings and the introduction of the new WNKA model without independent evidence provided in the abstract.

axioms (1)
  • domain assumption The structure is a semiring
    The language is parametric on a semiring to handle different quantities uniformly.
invented entities (1)
  • Weighted NetKAT Automata (WNKA) no independent evidence
    purpose: Capturing the stateful behavior of the language for operational semantics and enabling decision procedures
    Described as a novel model introduced in this work.

pith-pipeline@v0.9.0 · 5425 in / 1383 out tokens · 49688 ms · 2026-05-10T11:54:24.106301+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

46 extracted references · 30 canonical work pages

  1. [1]

    Domain theory

    Samson Abramsky and Achim Jung. Domain theory. InHandbook of logic in computer science (vol. 3) semantic structures, pages 1–168. 1995

    1995

  2. [2]

    Plb: congestion signals are simple and effective for network load balancing,

    Kinan Dak Albab, Jonathan DiLorenzo, Stefan Heule, Ali Kheradmand, Steffen Smolka, Konstantin Weitz, Muhammad Timarzi, Jiaqi Gao, and Minlan Yu. Switchv: Automated SDN switch validation with P4 models. InProceedings of the ACM SIGCOMM Conference, pages 365–379, 2022. doi: 10.1145/3544216.3544220

    work page doi:10.1145/3544216.3544220 2022

  3. [3]

    What’s decidable about weighted automata?Information and Computation, 282:104651, 2022

    Shaull Almagor, Udi Boker, and Orna Kupferman. What’s decidable about weighted automata?Information and Computation, 282:104651, 2022. ISSN 0890-5401. doi: https://doi.org/10.1016/j.ic.2020.104651. URL https://www. sciencedirect.com/science/article/pii/S0890540120301395. Special issue on 9th International Workshop Weighted Automata: Theory and Application...

    work page doi:10.1016/j.ic.2020.104651 2022

  4. [4]

    Netkat: semantic foundations for networks.SIGPLAN Not., 49(1):113–126, January 2014

    Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. Netkat: semantic foundations for networks.SIGPLAN Not., 49(1):113–126, January 2014. ISSN 0362-1340. doi: 10.1145/2578855.2535862. URL https://doi.org/10.1145/2578855.2535862

    work page doi:10.1145/2578855.2535862 2014

  5. [5]

    The NetKAT authors. Netkat. https://github.com/google/netkat, 2025

    2025

  6. [6]

    Pro- ceedings of the ACM on Programming Languages6(OOPSLA1), 1–30 (2022)

    Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler. Weighted programming: a programming paradigm for specifying mathematical models.Proc. ACM Program. Lang., 6(OOPSLA1), April 2022. doi: 10.1145/3527310. URL https://doi.org/10.1145/3527310

    work page doi:10.1145/3527310 2022

  7. [7]

    Cambridge University Press, Cambridge, UK, 2010

    Jean Berstel and Christophe Reutenauer.Noncommutative Rational Series with Applications, volume 137 ofEncyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, UK, 2010. ISBN 978-0-521-19022-0

    2010

  8. [8]

    Bloom and Zoltán Ésik.Matrix Iteration Theories, pages 289–351

    Stephen L. Bloom and Zoltán Ésik.Matrix Iteration Theories, pages 289–351. Springer Berlin Heidelberg, Berlin, Heidelberg, 1993. ISBN 978-3-642-78034-9. doi: 10.1007/978-3-642-78034-9_10. URL https://doi.org/10.1007/978-3-642- 78034-9_10

    work page doi:10.1007/978-3-642-78034-9_10 1993

  9. [9]

    Bonsangue, Helle H

    Filippo Bonchi, Marcello M. Bonsangue, Helle H. Hansen, Prakash Panangaden, Jan J. M. M. Rutten, and Alexandra Silva. Algebra-coalgebra duality in brzozowski’s minimization algorithm.ACM Trans. Comput. Logic, 15(1), March

  10. [10]

    doi: 10.1145/2490818

    ISSN 1529-3785. doi: 10.1145/2490818. URL https://doi.org/10.1145/2490818

    work page doi:10.1145/2490818

  11. [11]

    A core quantitative coeffect calculus

    Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A core quantitative coeffect calculus. In Zhong Shao, editor,Programming Languages and Systems, pages 351–370, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. ISBN 978-3-642-54833-8

    2014

  12. [12]

    and Kuich, W

    Manfred Droste and Werner Kuich.Semirings and Formal Power Series, pages 3–28. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009. ISBN 978-3-642-01492-5. doi: 10.1007/978-3-642-01492-5_1. URL https://doi.org/10.1007/978-3-642- 01492-5_1

    work page doi:10.1007/978-3-642-01492-5_1 2009

  13. [13]

    Iteration semirings

    Zoltán Ésik. Iteration semirings. InDevelopments in Language Theory, volume 5257 ofLecture Notes in Computer Science, pages 1–20. Springer, 2008

    2008

  14. [14]

    A coalgebraic decision procedure for netkat.SIGPLAN Not., 50(1):343–355, January 2015

    Nate Foster, Dexter Kozen, Mae Milano, Alexandra Silva, and Laure Thompson. A coalgebraic decision procedure for netkat.SIGPLAN Not., 50(1):343–355, January 2015. ISSN 0362-1340. doi: 10.1145/2775051.2677011. URL https://doi- org.proxy.library.cornell.edu/10.1145/2775051.2677011

    work page doi:10.1145/2775051.2677011 2015

  15. [15]

    Probabilistic netkat

    Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic netkat. In Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632, page 282–309, Berlin, Heidelberg, 2016. Springer-Verlag. ISBN 9783662494974. doi: 10.1007/978-3-662-49498-1_12. URL https: //doi.org/10.1007/978-3-662...

    work page doi:10.1007/978-3-662-49498-1_12 2016

  16. [16]

    A categorical approach to probability theory

    Michèle Giry. A categorical approach to probability theory. In B. Banaschewski, editor,Categorical Aspects of Topology and Analysis, pages 68–85, Berlin, Heidelberg, 1982. Springer Berlin Heidelberg. ISBN 978-3-540-39041-1

    1982

  17. [17]

    Golan.Partially-Ordered Semirings, pages 223–237

    Jonathan S. Golan.Partially-Ordered Semirings, pages 223–237. Springer Netherlands, Dordrecht, 1999. ISBN 978-94- 015-9333-5. doi: 10.1007/978-94-015-9333-5_20. URL https://doi.org/10.1007/978-94-015-9333-5_20

    work page doi:10.1007/978-94-015-9333-5_20 1999

  18. [18]

    and Karvounarakis, G

    Todd J. Green, Grigoris Karvounarakis, and Val Tannen. Provenance semirings. InProceedings of the Twenty-Sixth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS ’07, page 31–40, New York, NY, USA, 2007. Association for Computing Machinery. ISBN 9781595936851. doi: 10.1145/1265530.1265535. URL https://doi.org/10.1145/1265530.1265535

    work page doi:10.1145/1265530.1265535 2007

  19. [19]

    Griffin and Joäo Luís Sobrinho

    Timothy G. Griffin and Joäo Luís Sobrinho. Metarouting. InProceedings of the ACM SIGCOMM Conference, pages 1–12,

  20. [20]

    doi: 10.1145/1080091.1080094. Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 240. Publication date: June 2026. 240:24 Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Bøving, Nate Foster, and Alexandra Silva

    work page doi:10.1145/1080091.1080094 2026

  21. [21]

    Donovan, Brandon Schlinker, Nick Feamster, Jennifer Rexford, Scott Shenker, Russ Clark, and Ethan Katz-Bassett

    Arpit Gupta, Laurent Vanbever, Muhammad Shahbaz, Sean P. Donovan, Brandon Schlinker, Nick Feamster, Jennifer Rexford, Scott Shenker, Russ Clark, and Ethan Katz-Bassett. Sdx: a software defined internet exchange. SIGCOMM ’14, page 551–562, New York, NY, USA, 2014. Association for Computing Machinery. ISBN 9781450328364. doi: 10.1145/2619239.2626300. URL ht...

    work page doi:10.1145/2619239.2626300 2014

  22. [22]

    B4: experience with a globally-deployed software defined wan.SIGCOMM Comput

    Sushant Jain, Alok Kumar, Subhasree Mandal, Joon Ong, Leon Poutievski, Arjun Singh, Subbaiah Venkata, Jim Wanderer, Junlan Zhou, Min Zhu, Jon Zolla, Urs Hölzle, Stephen Stuart, and Amin Vahdat. B4: experience with a globally-deployed software defined wan.SIGCOMM Comput. Commun. Rev., 43(4):3–14, August 2013. ISSN 0146-4833. doi: 10.1145/2534169.2486019. U...

    work page doi:10.1145/2534169.2486019 2013

  23. [23]

    Validating datacenters at scale

    Karthick Jayaraman, Nikolaj Bjørner, Jitu Padhye, Amar Agrawal, Ashish Bhargava, Paul-Andre C Bissonnette, Shane Foster, Andrew Helwer, Mark Kasten, Ivan Lee, Anup Namdhari, Haseeb Niaz, Aniruddha Parkhi, Hanukumar Pinnamraju, Adrian Power, Neha Milind Raje, and Parag Sharma. Validating datacenters at scale. InProceedings of the ACM SIGCOMM Conference, pa...

    work page doi:10.1145/3341302.3342094 2019

  24. [24]

    Donald M. Kaplan. Regular expressions and the equivalence of programs.J. Comput. Syst. Sci., 3(4):361–386, 1969. doi: 10.1016/S0022-0000(69)80027-9. URL https://doi.org/10.1016/S0022-0000(69)80027-9

    work page doi:10.1016/s0022-0000(69)80027-9 1969

  25. [25]

    On limits in complete semirings.Semigroup Forum, 45(1):148–165, Dec 1992

    Georg Karner. On limits in complete semirings.Semigroup Forum, 45(1):148–165, Dec 1992. ISSN 1432-2137. doi: 10.1007/BF03025757. URL https://doi.org/10.1007/BF03025757

    work page doi:10.1007/bf03025757 1992

  26. [26]

    Kleene algebra with tests.ACM Trans

    Dexter Kozen. Kleene algebra with tests.ACM Trans. Program. Lang. Syst., 19(3):427–443, 1997. doi: 10.1145/256167. 256195. URL https://doi.org/10.1145/256167.256195

    work page doi:10.1145/256167 1997

  27. [27]

    The equality problem for rational series with multiplicities in the tropical semiring is undecidable

    Daniel Krob. The equality problem for rational series with multiplicities in the tropical semiring is undecidable. In Proceedings of the 19th International Colloquium on Automata, Languages and Programming, ICALP ’92, page 101–112, Berlin, Heidelberg, 1992. Springer-Verlag. ISBN 3540557199

    1992

  28. [28]

    Some consequences of a fatou property of the tropical semiring.Journal of Pure and Applied Algebra, 93 (3):231–249, 1994

    Daniel Krob. Some consequences of a fatou property of the tropical semiring.Journal of Pure and Applied Algebra, 93 (3):231–249, 1994. ISSN 0022-4049. doi: https://doi.org/10.1016/0022-4049(94)90090-6. URL https://www.sciencedirect. com/science/article/pii/0022404994900906

    work page doi:10.1016/0022-4049(94)90090-6 1994

  29. [29]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 2011

    Werner Kuich.Algebraic Systems and Pushdown Automata, pages 228–256. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. ISBN 978-3-642-24897-9. doi: 10.1007/978-3-642-24897-9_11. URL https://doi.org/10.1007/978-3-642- 24897-9_11

    work page doi:10.1007/978-3-642-24897-9_11 2011

  30. [30]

    Larsen, Stefan Schmid, and Bingtian Xue

    Kim G. Larsen, Stefan Schmid, and Bingtian Xue. Wnetkat: A weighted sdn programming and verification language,

  31. [31]

    URL https://arxiv.org/abs/1608.08483

    work page arXiv

  32. [32]

    Springer-Verlag, Berlin, Heidelberg, 2001

    Jean-Yves Le Boudec and Patrick Thiran.Network calculus: a theory of deterministic queuing systems for the Internet. Springer-Verlag, Berlin, Heidelberg, 2001. ISBN 354042184X

    2001

  33. [33]

    Galois internship round 2: A second summer intern experience

    Mark Moeller. 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. Ac- cessed: 2025-11-13

    2025

  34. [34]

    Katch: A fast symbolic verifier for netkat.Proc

    Mark Moeller, Jules Jacobs, Olivier Savary Bélanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, and Alexandra Silva. Katch: A fast symbolic verifier for netkat.Proc. ACM Program. Lang., 8(PLDI):1905–1928, 2024. doi: 10.1145/3656454. URL https://doi.org/10.1145/3656454

    work page doi:10.1145/3656454 1905

  35. [35]

    Active learning of symbolic netkat automata.Proc

    Mark Moeller, Tiago Ferreira, Thomas Lu, Nate Foster, and Alexandra Silva. Active learning of symbolic netkat automata.Proc. ACM Program. Lang., 9(PLDI), June 2025. doi: 10.1145/3729295. URL https://doi.org/10.1145/3729295

    work page doi:10.1145/3729295 2025

  36. [36]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 2009

    Mehryar Mohri.Weighted Automata Algorithms, pages 213–254. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009

    2009

  37. [37]

    Completeness of finitely weighted kleene algebra with tests

    Igor Sedlár. Completeness of finitely weighted kleene algebra with tests. In George Metcalfe, Thomas Studer, and Ruy de Queiroz, editors,Logic, Language, Information, and Computation, pages 210–224, Cham, 2024. Springer Nature Switzerland. ISBN 978-3-031-62687-6

    2024

  38. [38]

    Kleene algebra with tests for weighted programs

    Igor Sedlár. Kleene algebra with tests for weighted programs. In2023 IEEE 53rd International Symposium on Multiple- Valued Logic (ISMVL), pages 111–116, 2023. doi: 10.1109/ISMVL57333.2023.00031

    work page doi:10.1109/ismvl57333.2023.00031 2023

  39. [39]

    PhD thesis, INDIAN INSTITUTE OF TECHNOL- OGY DELHI, 2021

    Avaljot Singh.Cost InterNetKAT: Basics of Algebraic Network Routing. PhD thesis, INDIAN INSTITUTE OF TECHNOL- OGY DELHI, 2021

    2021

  40. [40]

    Cantor meets scott: semantic foundations for probabilistic networks.SIGPLAN Not., 52(1):557–571, January 2017

    Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. Cantor meets scott: semantic foundations for probabilistic networks.SIGPLAN Not., 52(1):557–571, January 2017. ISSN 0362-1340. doi: 10.1145/ 3093333.3009843. URL https://doi.org/10.1145/3093333.3009843

    work page doi:10.1145/3093333.3009843 2017

  41. [41]

    Guarded kleene algebra with tests: verification of uninterpreted programs in nearly linear time.Proc

    Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded kleene algebra with tests: verification of uninterpreted programs in nearly linear time.Proc. ACM Program. Lang., 4(POPL), December

  42. [42]

    URL https://doi.org/10.1145/3371129

    doi: 10.1145/3371129. URL https://doi.org/10.1145/3371129

    work page doi:10.1145/3371129

  43. [43]

    Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva

    Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva. Scalable verification of probabilistic networks. InProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, page 190–203, New York, NY, USA, 2019. Association for Computing Machinery. ISBN 9781450367...

    work page doi:10.1145/3314221.3314639 2019

  44. [44]

    An algebraic theory of dynamic network routing.IEEE/ACM Transactions on Networking (ToN), 13 (5):1160–1173, October 2005

    João Luís Sobrinho. An algebraic theory of dynamic network routing.IEEE/ACM Transactions on Networking (ToN), 13 (5):1160–1173, October 2005. doi: 10.1109/TNET.2005.857111

    work page doi:10.1109/tnet.2005.857111 2005

  45. [45]

    Weighted GKAT: Completeness and Complexity

    Spencer Van Koevering, Wojciech Różowski, and Alexandra Silva. Weighted GKAT: Completeness and Complexity. In Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, and Gabriele Puppis, editors,52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025), volume 334 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 1...

    work page doi:10.4230/lipics.icalp.2025.172 2025

  46. [46]

    𝑝is𝑟-safe

    Jacob Wasserstein. Guarded NetKAT: Soundness, partial-completeness, decidability. May 2023. doi: 10.7298/Y5X5-JR17. URL https://hdl.handle.net/1813/113959. Publisher: Cornell University Library. Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 240. Publication date: June 2026. 240:26 Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Bøving, ...

    work page doi:10.7298/y5x5-jr17 2023