Pith. sign in

REVIEW 4 major objections 5 minor 67 references

This paper introduces wSPPs, a decision-tree-like data structure that computes the exact semantics of weighted network policies—including loops—for any semiring with a computable star, and attaches witness paths to Pareto-optimal trade-offs

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-02 02:06 UTC pith:EB4T5TEY

load-bearing objection A genuinely new semiring-generic engine for quantitative NetKAT with a strong formal core, some artifact gaps, and one fixable circularity in the star termination proof. the 4 major comments →

arxiv 2607.14420 v1 pith:EB4T5TEY submitted 2026-07-15 cs.PL

A Fast Quantitative Analyzer for NetKAT

Thomas Lu (1) , Qiancheng Fu (1) , Kevin Batz (1) , Oliver B{\o}ving (2) , Tiago Ferreira (3) , Mark Moeller (1) , Nate Foster (4 , 5)
show 5 more authors
Alexandra Silva (1) ((1) Cornell University (2) Technical University of Denmark (3) University College London (4) EPFL (5) Jane Street)
This is my paper
classification cs.PL
keywords weighted NetKATsymbolic packet programssemiringKleene starPareto frontiermulti-objective network analysisnetwork verificationtrace-carrying semiring
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Network engineers need quantitative answers—latency, bandwidth, failure probability, and trade-offs between them—not just reachability. This paper builds a single analyzer for such questions by working with weighted NetKAT, a language in which every forwarding action carries a weight drawn from a semiring, and the semiring choice decides what quantity is tracked. The central invention is the weighted symbolic packet program (wSPP), a decision-tree-like representation that compiles a weighted policy into a compact object on which every operation, including the potentially infinite Kleene star, is computed symbolically and exactly. The paper further adds trace-carrying Pareto semirings, which report not only Pareto-optimal latency–bandwidth frontiers but also a witnessing network path for each point. Because the construction is generic in the semiring and formally verified, a single engine covers Boolean, probabilistic, and multi-objective analyses and scales to real topologies, making design-time comparisons such as Fat-tree versus Jellyfish automatic.

Core claim

The central claim is Theorem 4.12: for every weighted NetKAT policy over a semiring that has a computable star operation matching the semantics of iteration, there is an efficiently computable wSPP that is semantically equivalent to the policy, and any desired weight can be read off in one traversal. The hard part is Kleene star: weighted iteration may climb forever, so instead of finite unfolding, the algorithm performs symbolic state elimination—removing one entry of the underlying finite matrix at a time and emitting factors whose infinite sums collapse to the semiring's star operation. The same framework extends to Pareto and trace-carrying Pareto semirings, where the trace order is deli

What carries the argument

The central object is the wSPP: a decision tree whose nodes branch on a packet field, first on input value then output value, with leaves drawn from the semiring—effectively a finite symbolic matrix of the policy's weighted packet relation. The load-bearing identity is the star-coherence condition of the embedding (Definition 4.3(iii)): the computable star operation ⊛ on the chosen semiring must exactly equal the semantic infinite sum that defines iteration, which is what lets the star algorithm delegate all infinite summation to ⊛. Around this, the star algorithm's state-elimination passes, together with the trace-carrying Pareto semiring's absorbent trace order (longer traces are dominated

Load-bearing premise

The load-bearing premise is Definition 4.3(iii)—that for every weight in the chosen semiring, the finitely programmable star operation ⊛ returns exactly the value of the semantic infinite sum defining iteration; if some quantity's iteration lacks a computable star (unbounded chains, convex expected values), the compiled wSPP no longer denotes the policy's true behavior.

What would settle it

Fix the probability semiring and consider the policy (1/2⊙skip)*. Its semantic weight from a packet to itself is the geometric series 1 + 1/2 + 1/4 + ... = 2. If an implementation of the star operation on this semiring returned ∞ (as it would for many ad-hoc closed forms), the compiled wSPP would report ∞ instead of 2; more generally, exhibiting any single weight a in a proposed embeddable semiring for which a⊛ differs from the true infinite sum sup_n Σ_{i≤n} a^i would directly falsify the theorem's guarantee.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • A single semiring-generic engine can reproduce Boolean reachability, probabilistic reachability, latency, bandwidth, and multi-objective Pareto analysis without changing the underlying data structure.
  • Kleene star is computed exactly rather than by bounded unfolding, so probabilities and other iterated quantities receive their true infinite-series values.
  • Trace-carrying Pareto semirings deliver a witnessing path for each Pareto-optimal point, recovering per-path information that a dup-free semantics would otherwise lose.
  • Canonicalization makes semantic equivalence coincide with syntactic equality of wSPPs, enabling hash-based sharing and caching during compilation.
  • Design-time questions, such as which topology and routing scheme best balance latency, bandwidth, and path diversity, can be answered automatically at the scale of data-center networks.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The exactness of the approach rests on semiring-specific closed forms for iteration; quantities whose iteration has no finite closed form—such as fully probabilistic multi-objective expectations or unbounded cost chains—will need a different mechanism, as the paper's future-work section also suggests.
  • The subsequence-based trace order means reported witnesses are shortest modulo detours: two routes that differ only by inserted events are conflated. Engineers who need every equal-cost route, not one representative, would need a different trace order.
  • Canonicalization plus semantic-equivalence-as-syntactic-equality suggests an incremental verification workflow: a local change to a policy could be recompiled by reusing unchanged wSPP subtrees rather than restarting from scratch.
  • The measured overhead of witness traces grows with the width of Pareto frontiers rather than network size; on adversarial instances with very wide frontiers, trace-carrying mode will degrade more steeply than plain Pareto mode, so its use should be guided by expected frontier width.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper develops weighted symbolic packet programs (wSPPs), a decision-tree-style data structure for computing the semantics of dup-free weighted NetKAT (wNetKAT) over an embeddable star semiring. It gives structural compilation rules for all policy constructors, with the main technical contribution being a multi-pass Kleene-star algorithm (Fig. 9) that symbolically eliminates entries of a wSPP node. It then introduces Pareto frontier semirings and trace-carrying Pareto semirings, so that multi-objective frontiers are computed together with witness paths. The authors report a 53k-line Lean formalization and a 9k-line Rust implementation (Neko), benchmark against KATch, KATch2, McNetKAT, and Storm, and apply the tool to a Fat-tree vs. Jellyfish design study.

Significance. If the load-bearing issues below are resolved, this is a strong and significant contribution. The semiring-parametric design is a natural generalization of KATch's SPPs, and the explicit star-semiring embedding in Definition 4.3 is a well-designed interface that makes the mathematical assumptions visible. The trace-carrying Pareto construction is novel and convincingly motivated. The paper also ships an unusually large machine-checked development (53k lines of Lean), and the empirical evaluation includes cross-tool agreement checks, ablation studies, and a realistic multi-objective case study. The stated restrictions to bounded cost monoids and the exclusion of convex probabilistic frontiers are honest and are not hidden. The main concerns are three local but central proof obligations: the termination proof of Star, the unproved canonicalization theorem, and the imprecise statement of Theorem 5.3.

major comments (4)
  1. [§4.4 (Fig. 9 and the termination paragraph after Lemma 4.10)] The proof of Theorem 4.11 is circular as written. Termination is argued via a lexicographic measure, but the text says: 'Recursive calls decrease the first component: by well-formedness, sub-wSPPs omit the root field and their stars mention no new fields (Theorem 4.11), so the closures do not reintroduce it.' The property 'their stars mention no new fields' is part of Theorem 4.11, the very theorem under proof. The appendix already contains the correct simultaneous premise in Lemma B.14 ('If Star(σ) is sound on all wSPP σ that operate on fields greater than f'), but the main termination argument does not invoke it. Please restructure Theorem 4.11 as a simultaneous induction on |fields(ρ)| (or on the field ordering) that carries termination, well-formedness/no-new-fields, and soundness together. Without this, Theorem 4.12's computability claim and Corollary 4.13 do not follow from the tex
  2. [§6.1, Theorem 6.1] Theorem 6.1 states that semantic equivalence of wNetKAT policies is equivalent to syntactic equality of their canonical wSPPs, but no proof is given in the manuscript, nor is there a statement that this theorem is part of the Lean formalization. This claim is load-bearing for Neko's caching: the implementation reuses results for syntactically equal canonical wSPPs, and if canonicalization ever conflated non-equivalent policies, the benchmark results would be unsound. Please either provide a proof sketch or an explicit pointer to the formalized theorem. If the theorem is intended only as an optimization heuristic, the text should say so and explain what degree of sharing is actually guaranteed.
  3. [§5.1, Theorem 5.3] Theorem 5.3 is stated without a proof, and its hypothesis is imprecise: 'such that the star of every finitely generated lower set is finitely generated such as any product of bounded factors' is not a well-formed condition. This theorem is the only bridge from finite frontier semirings to the ω-continuous Pareto semiring Par(T), so it is load-bearing for applying Theorem 4.12 to Pareto and trace-carrying weights. Please state a precise condition (e.g., T is a finite product of bounded po-monoids in the sense of Definition A.2, or an explicit well-foundedness condition under which the star iteration in Definition 5.2 stabilizes), and give a proof sketch or a precise reference to the formalization, noting where boundedness is used and how Example A.1 is excluded.
  4. [§4.1, Definition 4.3(iii)] The correctness of the whole pipeline rests on the assumption that the computable operation ⊛ on A exactly matches the semantic infinite sum on S. The paper is explicit about this, and the appendices give several instances, but the central Theorem 4.12 is conditional on this matching. I do not regard this as a flaw, because the paper states the restriction clearly and even points to the unresolved cases (unbounded chains, convex probabilistic frontiers). However, the introduction and abstract should be more careful not to overstate the range of 'quantitative network properties' supported; in particular, fully probabilistic multi-objective trade-offs are not covered, as the Future Work section correctly acknowledges.
minor comments (5)
  1. [§6.1, paragraph 2] The sentence 'Although deciding semantic equivalence is not the focus of wNetKAT, Although deciding semantic equivalence is not the focus of wNetKAT, canonicalization remains valuable' contains a duplicated clause.
  2. [Theorem 5.3; proof status] The paper says 'The key result on frontier semirings is the following theorem' but then gives no proof or appendix reference. Since the Lean artifact is the main evidence for several theoretical claims, please include a theorem-to-file mapping for Theorems 4.7, 4.11, 4.12, 5.3, 5.5, 5.6, and 6.1.
  3. [Artifact / Reproducibility] The anonymized Lean repository URL is given, but no commit hash or file manifest is provided. The expression 'a checkpoint has been submitted as supplementary material' is too vague for a paper that makes strong verification claims. Please provide a versioned artifact identifier and a short description of which files contain each theorem.
  4. [§6.2, experimental setup] The sentence 'conducted using an Intel Xeon Gold 6348 CPU with 20GB memory- and 20min time-limit' has a typographical issue ('memory-' should be 'memory').
  5. [§5.2, trace order narrative] The trace order definition is mathematically clear, but the phrase 'descending from (q,v) means worsening the cost vector and inserting arbitrary extra events' is initially confusing because the order is oriented so that 'bigger is better'. A short remark that maximal elements carry shortest traces would help the reader.

Circularity Check

1 steps flagged

One localized proof self-reference in the star termination argument; no substantive circularity in the compiler or Pareto/trace results.

specific steps
  1. other [Section 4.4, Termination paragraph before Theorem 4.11 (see also Appendix B.14)]
    "Recursive calls decrease the first component: by well-formedness, sub-wSPPs omit the root field and their stars mention no new fields (Theorem 4.11), so the closures do not reintroduce it."

    The termination proof of Star invokes Theorem 4.11--the statement being proved--to justify that stars of recursive calls introduce no new fields. Since Theorem 4.11 includes both termination and the field-containment property, this is a self-referential proof step unless it is read as a simultaneous induction on |fields(rho)|, which the prose does not state. Appendix Lemma B.14 supplies the analogous induction hypothesis only for soundness, not for termination/field-containment; hence the main-text proof as written is not self-contained. The flaw is repairable and the Lean artifact may supply the missing induction, so it is a localized circularity rather than a reduction of the result to its inputs.

full rationale

The central wSPP compilation Theorem 4.12 is parametric and parameter-free: it is proven by structural recursion and the star algorithm's correctness (Lemma 4.10, Appendix B.14) uses an explicit induction hypothesis on fields. Definition 4.3(iii) is a stated assumption, not a fitted input: the paper explicitly shows (Example A.1) that without a matching computable star the construction fails. The Pareto and trace-carrying semirings are self-contained under stated boundedness conditions; Theorem 5.5 is proved directly from the trace order and boundedness, and the finiteness of frontiers is a theorem, not an input. Self-citations to wNetKAT [61] are to a prior semantic framework and are not load-bearing; the new wSPP and trace-carrying results are proved independently, and the benchmarks are cross-validated against KATch, McNetKAT, and Storm. The only circularity located is the termination paragraph's appeal to Theorem 4.11 itself; as written this is a proof-level self-reference, but it is localized and repairable by the simultaneous induction that Lemma B.14 and the Lean formalization indicate. Hence the paper does not reduce its predictions to its inputs; score 2 reflects the one minor, non-substantive circular step.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 2 invented entities

No fitted parameters: all constants are inputs from the chosen semiring, and no hand-tuned numbers are introduced to make benchmarks or derivations work. The main axioms are the star-semiring embedding assumption and the boundedness of the cost monoid, both stated in the paper and both excluding some multi-objective probabilistic settings.

axioms (4)
  • domain assumption S is an ω-continuous semiring and A is a computable star semiring embedded into S via ι satisfying ι(a⊛) = ι(a)* (Definition 4.3).
    Required to define countable sums for Kleene star and to replace the semantic star by a computable star operation on the finite representations actually used by wSPPs.
  • standard math The wNetKAT equational laws in Figure 6 and the two star laws in Theorem 3.3 hold.
    These laws are consequences of ω-continuous (Conway) semirings and are used throughout the compiler correctness proofs, especially in the star algorithm.
  • domain assumption T is a bounded partially ordered monoid with monotone multiplication, and the star of every finitely generated lower set is finitely generated (Theorem 5.3).
    This guarantees that Pareto frontiers and trace-carrying frontiers remain finite under Kleene star. It is explicitly acknowledged in Future Work that fully probabilistic multi-objective analysis does not form such a monoid.
  • domain assumption The set of fields F and values Val are finite, with a fixed total order on fields.
    Packet space Pk = F -> Val is finite, which is standard for NetKAT and needed for well-formedness and termination of the recursive star algorithm.
invented entities (2)
  • Weighted symbolic packet programs (wSPPs) no independent evidence
    purpose: Compact symbolic representation of weighted packet relations for all wNetKAT policy constructors, including Kleene star.
    Introduced in this paper as an internal formal/algorithmic object; it has no independent empirical confirmation outside the paper, though it is formalized in Lean and implemented in Rust.
  • Trace-carrying Pareto semiring Fr(T x Σ*) no independent evidence
    purpose: Attach witness traces to Pareto-optimal cost vectors while keeping frontiers finite via the ε-isolating trace order.
    A new construction in this paper; correctness is shown in Theorems 5.5 and 5.6, but it has no independent external falsifiable handle.

pith-pipeline@v1.3.0-alltime-deepseek · 51038 in / 11314 out tokens · 111852 ms · 2026-08-02T02:06:29.890143+00:00 · methodology

0 comments
read the original abstract

When designing a network, engineers must navigate trade-offs (e.g., one topology offers more aggregate bandwidth, another lower latency or better resilience) that demand reasoning about quantitative properties. We present a fast analyzer for quantitative network properties based on weighted NetKAT (wNetKAT), a domain-specific language that provides a semantic foundation for quantitative reasoning by modeling network behavior using weights drawn from a semiring. At the core of our development is the design of a symbolic data structure -- weighted symbolic packet programs (wSPPs) -- that compactly represent the semantics of weighted policies, for which a direct implementation would be intractable. We show how to compute all policy constructs symbolically; unsurprisingly, the crux is Kleene star, for which we design a tailored algorithm. We further develop trace-carrying Pareto semirings, which compute multi-objective frontiers together with the network paths that realize them. We formalize the development in Lean and provide an optimized Rust implementation. Being parametric on a semiring, our implementation covers both classical and quantitative analyses: we show that it is competitive with KATch, a heavily optimized Boolean-reachability verifier, and orders of magnitude faster than McNetKAT and Storm on probabilistic analyses. A case study comparing Fat-tree and Jellyfish data-center topologies shows the framework supports multi-objective design-time analysis.

Figures

Figures reproduced from arXiv: 2607.14420 by (2) Technical University of Denmark, (3) University College London, (4) EPFL, 5), (5) Jane Street), Alexandra Silva (1) ((1) Cornell University, Kevin Batz (1), Mark Moeller (1), Nate Foster (4, Oliver B{\o}ving (2), Qiancheng Fu (1), Thomas Lu (1), Tiago Ferreira (3).

Figure 1
Figure 1. Figure 1: A probabilistic policy 𝑝 (left) and its compiled wSPP 𝑝ˆ (right). 𝑞 ≜  sw = 1 ; st = rdy ; [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The policy 𝑞 (left) obtained from iterating the policy 𝑝 from [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The two-class bypass chain. The policy 𝑝 (𝑖 = 1, . . . , 4) over the Pareto semiring of latency–bandwidth frontiers (left); a literal weight { (ℓ, 𝑤) } charges ℓ ms and caps the bandwidth at 𝑤 Gb/s. The colored event letters log the billable events. The two frontiers of 𝑝 (right), shaded regions are the down-closed achievable trade-offs, the staircases their finite frontier representations, and each fronti… view at source ↗
Figure 4
Figure 4. Figure 4: Two paths between the same two hosts in two different topologies: A favors bandwidth, B favors latency; neither dominates the other. Formally, a weight pairs each cost vector with a log, and the weighting operator doubles as a logging primitive, and, since our wSPP compiler is semiring-agnostic, this enables the efficient, trace-carrying trade-off analysis. Now consider the colored event letters of [PITH_… view at source ↗
Figure 5
Figure 5. Figure 5: Syntax and semantics of (dup-free) wNetKAT over an 𝜔-continuous semiring S = (𝑆, +, · , 0, 1). Operator precedence, from strongest- to weakest-binding: (−)∗ , ¬, ∧, ∨, ⊙, ;, ⊕. Here, [𝑃] denotes the Iverson bracket into S: [𝑃] = 1 if the proposition 𝑃 holds and [𝑃] = 0 otherwise. 3 Weighted NetKAT This section recaps the fragment of wNetKAT used in this paper. Throughout, we fix a finite set F of fields an… view at source ↗
Figure 6
Figure 6. Figure 6: Linearity laws inherited from the semiring structure and packet algebra laws governing tests and assignments. 3.2 Equational Reasoning We write 𝑝 ≡ 𝑞 for semantic equivalence ⟦𝑝⟧ = ⟦𝑞⟧. On dup-free policies, ≡ agrees with the history-based semantics of full wNetKAT [61], so all results below apply unchanged in that setting. The data structure of Section 4 is manipulated by equational rewriting of policies,… view at source ↗
Figure 7
Figure 7. Figure 7: The three guises of a wSPP 𝜌: syntax (upper right), read-back policy (lower right), and the graphical representation as a tree (left). Vertices are labeled by the field the node branches on. For instance, (𝑓 ≠ 𝑣) Ó tests value 𝑣 and offers it no continuation (the empty row), while all other values pass unchanged into the default identity 1ˆ. Compound tests compiles as follows: conjunction compiles to seque… view at source ↗
Figure 8
Figure 8. Figure 8: A wSPP node is a finitely presented Val × Val matrix: the running example 𝜌 (Example 4.8), with the entry in row 𝑢 and column 𝑣 being the continuation taken when 𝑓 is rewritten from 𝑢 to 𝑣. Empty positions are 0ˆ. Example 4.8 (running example). Over A = Q ∞ ≥0 , consider the one-field wSPP 𝜌 = wspp 𝑓 , {1 ↦→ {1 ↦→ 1/2, 4 ↦→ 1 }, 2 ↦→ {1 ↦→ 1/2 }}, {1 ↦→ 1/5, 3 ↦→ 1/4 }, 1/3  , drawn on the left of [PITH_… view at source ↗
Figure 9
Figure 9. Figure 9: The wSPP star algorithm: symbolic elimination of the root node. ⌊𝑔(𝑥)⌋ denotes 𝑔(𝑥) if 𝑥 ∈ dom(𝑔) and 0ˆ otherwise; wide-hatted atoms denote their atomic wSPPs, a wide hat Π applies the ˆ;-product (Section 4.3). root field and their stars mention no new fields (Theorem 4.11), so the closures do not reintroduce it. Pass I update decreases the default-identity bit; advancing from Pass I to Pass II decreases … view at source ↗
Figure 10
Figure 10. Figure 10: A complete run of [PITH_FULL_IMAGE:figures/full_fig_p017_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Boolean reachability scalability: running time (left) and peak memory usage (right) . The crucial observation is that, since 𝜌 ′ neither tests nor assigns 𝑔, every write to 𝑔 made inside the middle star passes through 𝜌 ′ unchanged and is overwritten by the trailing 𝜎. Thus, the identity above stil holds if every descendant wSPP wspp(𝑔, ∅,𝑚, 0) in the 𝜎 inside the middle star is replaced by Éc𝑣∈dom(𝑚) 𝑚(𝑣… view at source ↗
Figure 12
Figure 12. Figure 12: Probabilistic reachability scalability: running time (left) and peak memory usage (right). much more involved than SPP which is a straightforward fixpoint iteration. The verified Lean trails in speed because it forgoes the sharing and caching optimizations employed by the other tools. Where those tools resolve a repeated computation with a single cache lookup, Lean must instead recompute the corresponding… view at source ↗
Figure 13
Figure 13. Figure 13: Case study results: Fat tree vs. Jellyfish analysis. (a, left) Scatterplot of Pareto-optimal points across the analyzed networks. (b, middle) Hotspot concentration, showing how many switches are needed to realize a given share of Pareto-optimal paths. (c, right) Pointwise network-to-network comparison of Pareto frontiers. Network Frontier Latency Latency Latency Bandwidth Bandwidth Bandwidth Topology + Po… view at source ↗
Figure 14
Figure 14. Figure 14: Embeddings 𝜄 : A ↩→ S of computable star semirings into the 𝜔-continuous semirings of common network quantities (cf. [61]). In the first six rows 𝜄 is the evident inclusion. The latency semiring is ordered by ≥, under which its unit 0 is the greatest element. 𝑎 ⊛ ≜ 0 for 𝑎 ≤ 0 and 𝑎 ⊛ ≜ 1 otherwise, and (iii) reduces to the observation that (1 − 𝑎) 𝑘 → 0 for 𝑎 > 0. △ In all rows of [PITH_FULL_IMAGE:figur… view at source ↗
Figure 15
Figure 15. Figure 15: compares the running time of Neko on F10 and Jellyfish topologies in both Pareto and trace-carrying Pareto modes. The running time of trace-carrying Pareto is only marginally higher than Pareto at around 5% on average. This is due to the fact that these networks, while having a large number of paths (400,000+ on larger networks), do not have wide Pareto frontiers (1.7 on average). ecmp 4-shortest 8-shorte… view at source ↗
Figure 16
Figure 16. Figure 16: Trace scaling: running time (c) and peak memory usage (d) of Pareto and trace-carrying Pareto [PITH_FULL_IMAGE:figures/full_fig_p048_16.png] view at source ↗

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

67 extracted references · 9 canonical work pages

  1. [1]

    Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. 2020. Tiramisu: Fast Multilayer Net- work Verification. In17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). USENIX Association, Santa Clara, CA, 201–219. https://www.usenix.org/conference/nsdi20/presentation/abhashkumar

    2020

  2. [2]

    Samson Abramsky and Achim Jung. 1995. Domain theory. InHandbook of Logic in Computer Science (Vol. 3): Semantic Structures. Oxford University Press, Inc., USA, 1–168

    1995

  3. [3]

    Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: Semantic Foundations for Networks. InThe 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14. ACM, 113–126. doi:10.1145/2535838.2535862

    arXiv 2014

  4. [4]

    Hu, Temesghen Kahsai, Bill Kocik, Evgenii Kotelnikov, Jure Kukovec, Sean McLaughlin, Jason Reed, Neha Rungta, John Sizemore, Mark A

    John Backes, Sam Bayless, Byron Cook, Catherine Dodge, Andrew Gacek, Alan J. Hu, Temesghen Kahsai, Bill Kocik, Evgenii Kotelnikov, Jure Kukovec, Sean McLaughlin, Jason Reed, Neha Rungta, John Sizemore, Mark A. Stalzer, Preethi Srinivasan, Pavle Subotic, Carsten Varming, and Blake Whaley. 2019. Reachability Analysis for AWS-Based Networks. InInternational ...

    2019

  5. [5]

    Iris Bahar, Erica A

    R. Iris Bahar, Erica A. Frohm, Charles M. Gaona, Gary D. Hachtel, Enrico Macii, Abelardo Pardo, and Fabio Somenzi

  6. [6]

    Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. 2017. A General Approach to Network Configuration Verification. InProceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM ’17). ACM, Los Angeles, CA, USA, 155–168. doi:10.1145/3098822.3098834

    arXiv 2017

  7. [7]

    Seshadhri, Enrico Carlesso, Chinchu Merine Joseph, Saurabh Kumar, Pavan Manikonda, Luiza Popa, Randy Ram, Steven Robinson, and Elizabeth Tennent

    Giacomo Bernardi, Ratul Mahajan, C. Seshadhri, Enrico Carlesso, Chinchu Merine Joseph, Saurabh Kumar, Pavan Manikonda, Luiza Popa, Randy Ram, Steven Robinson, and Elizabeth Tennent. 2026. RNG: Flat Datacenter Networks at Scale. arXiv:2604.15261 [cs.NI] https://arxiv.org/abs/2604.15261

    Pith/arXiv arXiv 2026

  8. [8]

    Stefano Bistarelli, Fabio Gadducci, Javier Larrosa, and Emma Rollon. 2008. A Soft Approach to Multi-objective Optimization. InLogic Programming, 24th International Conference, ICLP 2008 (Lecture Notes in Computer Science, Vol. 5366). Springer, 764–768. doi:10.1007/978-3-540-89982-2_73

    work page doi:10.1007/978-3-540-89982-2_73 2008

  9. [10]

    Randal E. Bryant. 1986. Graph-Based Algorithms for Boolean Function Manipulation.IEEE Trans. Computers35, 8 (1986), 677–691

    1986

  10. [11]

    Daggitt, Alexander J

    Matthew L. Daggitt, Alexander J. T. Gurney, and Timothy G. Griffin. 2018. Asynchronous convergence of policy-rich distributed Bellman-Ford routing protocols. InSIGCOMM. ACM, 103–116

    2018

  11. [12]

    Dannert, Erich Grädel, Matthias Naaf, and Val Tannen

    Katrin M. Dannert, Erich Grädel, Matthias Naaf, and Val Tannen. 2021. Semiring Provenance for Fixed-Point Logic. In CSL (LIPIcs, Vol. 183). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 17:1–17:22

    2021

  12. [13]

    Pedro Maristany de las Casas, Ralf Borndörfer, Antonio Sedeño-Noda, and Marc E. Pfetsch. 2023. Targeted Multiobjec- tive Dijkstra Algorithm.Networks82, 3 (2023), 277–298. doi:10.1002/net.22174

    work page doi:10.1002/net.22174 2023

  13. [14]

    Pedro Maristany de las Casas, Antonio Sedeño-Noda, and Ralf Borndörfer. 2021. An Improved Multiobjective Shortest Path Algorithm.Computers & Operations Research135 (2021), 105424. doi:10.1016/j.cor.2021.105424

    arXiv 2021

  14. [15]

    Daniel Deutch, Tova Milo, Sudeepa Roy, and Val Tannen. 2014. Circuits for Datalog Provenance. InICDT. OpenPro- ceedings.org, 201–212. A Fast Quantitative Analyzer for NetKAT 1:27

    2014

  15. [16]

    Manfred Droste and Werner Kuich. 2009. Semirings and Formal Power Series. InHandbook of Weighted Automata, Manfred Droste, Werner Kuich, and Heiko Vogler (Eds.). Springer, Berlin, Heidelberg, Chapter 1, 3–28. doi:10.1007/978- 3-642-01492-5_1

    doi:10.1007/978- 2009

  16. [17]

    Zoltán Ésik. 2008. Iteration Semirings. InDevelopments in Language Theory (Lecture Notes in Computer Science, Vol. 5257), Masami Ito and Masafumi Toyama (Eds.). Springer, Berlin, Heidelberg, 1–20. doi:10.1007/978-3-540-85780-8_1

    work page doi:10.1007/978-3-540-85780-8_1 2008

  17. [18]

    Zoltán Ésik and Werner Kuich. 2004. Inductive *-semirings.Theoretical Computer Science324, 1 (2004), 3–33

    2004

  18. [19]

    Kwiatkowska, Moshe Y

    Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. 2007. Multi-objective Model Checking of Markov Decision Processes. InTACAS (Lecture Notes in Computer Science, Vol. 4424). Springer, 50–65

    2007

  19. [20]

    Hélène Fargier, Pierre Marquis, Alexandre Niveau, and Nicolas Schmidt. 2014. A Knowledge Compilation Map for Ordered Real-Valued Decision Diagrams. InAAAI. AAAI Press, 1049–1055

    2014

  20. [21]

    Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein

  21. [22]

    Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu

    Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. 2011. Quantitative Multi- objective Verification for Probabilistic Systems. InTACAS (Lecture Notes in Computer Science, Vol. 6605). Springer, 112–127

    2011

  22. [23]

    Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. InProgramming Languages and Systems, Peter Thiemann (Ed.). Vol. 9632. Springer Berlin Heidelberg, Berlin, Heidelberg, 282–309. doi:10.1007/978-3-662-49498-1_12 Series Title: Lecture Notes in Computer Science

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

  23. [24]

    McGeer, and Jerry Chih-Yuan Yang

    Masahiro Fujita, Patrick C. McGeer, and Jerry Chih-Yuan Yang. 1997. Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation.Formal Methods Syst. Des.10, 2/3 (1997), 149–169

    1997

  24. [25]

    Timon Gehr, Sasa Misailovic, Petar Tsankov, Laurent Vanbever, Pascal Wiesmann, and Martin Vechev. 2018. Bayonet: probabilistic inference for networks. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation(Philadelphia, PA, USA)(PLDI 2018). Association for Computing Machinery, New York, NY, USA, 586–602. doi:10....

    arXiv 2018

  25. [26]

    Marc Geilen, Twan Basten, Bart Theelen, and Ralph Otten. 2007. An Algebra of Pareto Points.Fundamenta Informaticae 78, 1 (2007), 35–74. Conference version: ACSD 2005

    2007

  26. [27]

    Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. 2016. Fast Control Plane Analysis Using an Abstract Representation. InProceedings of the 2016 ACM SIGCOMM Conference (SIGCOMM ’16). ACM, Florianopolis, Brazil, 300–313. doi:10.1145/2934872.2934876

    arXiv 2016

  27. [28]

    2008.Graphs, Dioids and Semirings: New Models and Algorithms

    Michel Gondran and Michel Minoux. 2008.Graphs, Dioids and Semirings: New Models and Algorithms. Operations Research/Computer Science Interfaces Series, Vol. 41. Springer. doi:10.1007/978-0-387-75450-5

    work page doi:10.1007/978-0-387-75450-5 2008

  28. [29]

    Joshua Goodman. 1999. Semiring Parsing.Computational Linguistics25, 4 (1999), 573–605. https://aclanthology.org/J99- 4004/

    1999

  29. [30]

    Green, Grigoris Karvounarakis, and Val Tannen

    Todd J. Green, Grigoris Karvounarakis, and Val Tannen. 2007. Provenance Semirings. InProceedings of the Twenty-Sixth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS ’07). ACM, 31–40. doi:10.1145/ 1265530.1265535

    arXiv 2007

  30. [31]

    Griffin and João L

    Timothy G. Griffin and João L. Sobrinho. 2005. Metarouting. InSIGCOMM. ACM, 1–12

    2005

  31. [32]

    Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. 2020. The Probabilistic Model Checker Storm. doi:10.48550/arXiv.2002.07080 arXiv:2002.07080 [cs.SE]

    Pith/arXiv arXiv doi:10.48550/arxiv.2002.07080 2020

  32. [33]

    Christian Hopps. 2000. Analysis of an Equal-Cost Multi-Path Algorithm. RFC 2992. doi:10.17487/RFC2992

    doi:10.17487/rfc2992 2000

  33. [34]

    Jules Jacobs. 2025. KATch2: A Symbolic Verifier for Reversible NetKAT in Rust. https://github.com/julesjacobs/KATch2. Accessed: 2026-07-04

    2025

  34. [35]

    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. 2019. Validating datacenters at scale. InProceedings of the ACM Special Interest...

    arXiv 2019

  35. [36]

    Peyman Kazemian, Michael Chang, Hongyi Zeng, George Varghese, Nick McKeown, and Scott Whyte. 2013. Real Time Network Policy Checking Using Header Space Analysis. In10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13). USENIX Association, Lombard, IL, 99–111. https://www.usenix.org/conference/nsdi13/ technical-sessions/presentatio...

    2013

  36. [37]

    Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12). USENIX Association, San Jose, CA, 113–126. https://www.usenix.org/conference/nsdi12/technical-sessions/presentation/kazemian 1:28 Lu et al

    2012

  37. [38]

    Brighten Godfrey

    Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. 2013. VeriFlow: Verifying Network-Wide Invariants in Real Time. In10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13). USENIX Association, Lombard, IL, 15–27. https://www.usenix.org/conference/nsdi13/technical-sessions/ presentation/khurshid

    2013

  38. [39]

    Nguyen, Nickolas Falkner, Rhys Bowden, and Matthew Roughan

    Simon Knight, Hung X. Nguyen, Nickolas Falkner, Rhys Bowden, and Matthew Roughan. 2011. The Internet Topology Zoo.IEEE Journal on Selected Areas in Communications29, 9 (Oct. 2011), 1765–1775. doi:10.1109/JSAC.2011.111002

    Pith/arXiv arXiv 2011

  39. [40]

    Dexter Kozen. 1997. Kleene algebra with tests.ACM Trans. Program. Lang. Syst.19, 3 (May 1997), 427–443. doi:10. 1145/256167.256195

    arXiv 1997

  40. [41]

    Werner Kuich. 1991. Automata and Languages Generalized to𝜔-Continuous Semirings.Theoretical Computer Science 79, 1 (1991), 137–150. doi:10.1016/0304-3975(91)90147-T

    work page doi:10.1016/0304-3975(91)90147-t 1991

  41. [42]

    Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems. InProc. 23rd International Conference on Computer Aided Verification (CA V’11) (Lecture Notes in Computer Science, Vol. 6806), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer, 585–591. doi:10.1007/978-3-642-22110-1_47

    doi:10.1007/978-3-642-22110-1_47 2011

  42. [43]

    Yung-Te Lai and Sarma Sastry. 1992. Edge-Valued Binary Decision Diagrams for Multi-Level Hierarchical Verification. InDAC. IEEE Computer Society Press, 608–613

    1992

  43. [44]

    Javier Larrosa, Albert Oliveras, and Enric Rodríguez-Carbonell. 2010. Semiring-Induced Propositional Logic: Definition and Basic Algorithms. InLogic for Programming, Artificial Intelligence, and Reasoning, 17th International Conference, LPAR-17 (Lecture Notes in Computer Science, Vol. 6355). Springer, 332–347. doi:10.1007/978-3-642-17511-4_19

    work page doi:10.1007/978-3-642-17511-4_19 2010

  44. [45]

    2001.Network Calculus: A Theory of Deterministic Queuing Systems for the Internet

    Jean-Yves Le Boudec and Patrick Thiran. 2001.Network Calculus: A Theory of Deterministic Queuing Systems for the Internet. Lecture Notes in Computer Science, Vol. 2050. Springer-Verlag, Berlin, Heidelberg. doi:10.1007/3-540-45318-0

    work page doi:10.1007/3-540-45318-0 2001

  45. [46]

    Daniel J. Lehmann. 1977. Algebraic structures for transitive closure.Theoretical Computer Science4, 1 (1977), 59–76. doi:10.1016/0304-3975(77)90056-1

    doi:10.1016/0304-3975(77)90056-1 1977

  46. [48]

    Robert Manger. 2020. An Algebraic Framework for Multi-Objective and Robust Variants of Path Problems.Glasnik Matematički55, 1 (2020), 143–176. doi:10.3336/gm.55.1.12

    work page doi:10.3336/gm.55.1.12 2020

  47. [49]

    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.Proc. ACM Program. Lang.8, PLDI, Article 224 (June 2024), 24 pages. doi:10.1145/3656454

    doi:10.1145/3656454 2024

  48. [50]

    Mehryar Mohri. 2002. Semiring Frameworks and Algorithms for Shortest-Distance Problems.Journal of Automata, Languages and Combinatorics7, 3 (2002), 321–350. https://cs.nyu.edu/~mohri/pub/jalc.pdf

    2002

  49. [51]

    Kun Qian, Yongqing Xi, Jiamin Cao, Jiaqi Gao, Yichi Xu, Yu Guan, Binzhang Fu, Xuemei Shi, Fangbo Zhu, Rui Miao, Chao Wang, Peng Wang, Pengcheng Zhang, Xianlong Zeng, Eddie Ruan, Zhiping Yao, Ennan Zhai, and Dennis Cai

  50. [52]

    Yann Ramusat, Silviu Maniu, and Pierre Senellart. 2021. Provenance-Based Algorithms for Rich Queries over Graph Databases. InEDBT. OpenProceedings.org, 73–84

    2021

  51. [53]

    Fabian Ruffy, Jed Liu, Prathima Kotikalapudi, Vojtěch Havel, Hanneli Tavante, Rob Sherwood, Vladyslav Dubina, Volodymyr Peschanenko, Anirudh Sivaraman, and Nate Foster. 2023. P4Testgen: An Extensible Test Oracle For P4-16. InProceedings of the ACM SIGCOMM 2023 Conference (ACM SIGCOMM ’23). ACM, New York, NY, USA, 136–151. doi:10.1145/3603269.3604834

    arXiv 2023

  52. [54]

    S. N. Samborskii and A. A. Tarashchan. 1992. The Fourier Transform and Semirings of Pareto Sets. InIdempotent Analysis, V. P. Maslov and S. N. Samborskii (Eds.). Advances in Soviet Mathematics, Vol. 13. American Mathematical Society, Providence, RI, 139–150

    1992

  53. [55]

    Arjun Singh, Joon Ong, Amit Agarwal, Glen Anderson, Ashby Armistead, Roy Bannon, Seb Boving, Gaurav Desai, Bob Felderman, Paulie Germano, Anand Kanagala, Jeff Provost, Jason Simmons, Eiichi Tanda, Jim Wanderer, Urs Hölzle, Stephen Stuart, and Amin Vahdat. 2015. Jupiter Rising: A Decade of Clos Topologies and Centralized Control in Google’s Datacenter Netw...

    arXiv 2015

  54. [56]

    Brighten Godfrey

    Ankit Singla, Chi-Yao Hong, Lucian Popa, and P. Brighten Godfrey. 2012. Jellyfish: Networking Data Centers Randomly. In9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12). USENIX Association, San Jose, CA, 225–238. https://www.usenix.org/conference/nsdi12/technical-sessions/presentation/singla A Fast Quantitative Analyzer for NetKAT 1:29

    2012

  55. [57]

    Steffen Smolka, Spiridon Eliopoulos, Nate Foster, and Arjun Guha. 2015. A fast compiler for NetKAT. InProceedings of the 20th ACM SIGPLAN International Conference on Functional Programming. ACM, Vancouver BC Canada, 328–341. doi:10.1145/2784731.2784761

    arXiv 2015

  56. [58]

    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. 2019. Scalable verification of probabilistic networks. InProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, Phoenix AZ USA, 190–203. doi:10.1145/3314221.3314639

    arXiv 2019

  57. [59]

    Somasundaram and John S

    Kiran K. Somasundaram and John S. Baras. 2011. Solving Multi-metric Network Problems: An Interplay Between Idempotent Semiring Rules.Linear Algebra Appl.435, 10 (2011), 2473–2500. doi:10.1016/j.laa.2011.02.055

    work page doi:10.1016/j.laa.2011.02.055 2011

  58. [60]

    Radu Stoenescu, Dragos Dumitrescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. 2018. Debugging P4 Programs with Vera. InProceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication (SIGCOMM ’18). ACM, Budapest, Hungary, 518–532. doi:10.1145/3230543.3230548

    arXiv 2018

  59. [61]

    Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Bøving, Nate Foster, and Alexandra Silva. 2026. Weighted NetKAT: A Programming Language for Quantitative Network Verification.Proc. ACM Program. Lang.10, PLDI, Article 240 (June 2026), 24 pages. doi:10.1145/3808318

    doi:10.1145/3808318 2026

  60. [62]

    2023.Automating the Analysis and Improvement of Dynamic Programming Algorithms with Applications to Natural Language Processing

    Tim Vieira. 2023.Automating the Analysis and Improvement of Dynamic Programming Algorithms with Applications to Natural Language Processing. Ph. D. Dissertation. Johns Hopkins University, Baltimore, Maryland. https://jscholarship. library.jhu.edu/items/f78cc5e6-9dba-451f-b45c-6a390a255355

    2023

  61. [63]

    Nic Wilson. 2005. Decision Diagrams for the Computation of Semiring Valuations. InIJCAI. Professional Book Center, 331–336

    2005

  62. [64]

    Hongkun Yang and Simon S. Lam. 2013. Real-Time Verification of Network Properties Using Atomic Predicates. In 2013 21st IEEE International Conference on Network Protocols (ICNP). IEEE, Göttingen, Germany, 1–11. doi:10.1109/ ICNP.2013.6733614

    arXiv 2013

  63. [65]

    Jin Y. Yen. 1971. Finding the K Shortest Loopless Paths in a Network.Management Science17, 11 (1971), 712–716. doi:10.1287/mnsc.17.11.712

    doi:10.1287/mnsc.17.11.712 1971

  64. [66]

    Peng Zhang, Xu Liu, Hongkun Yang, Ning Kang, Zhengchang Gu, and Hao Li. 2020. APKeep: Realtime Verification for Real Networks. In17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). USENIX Association, Santa Clara, CA, 241–255. https://www.usenix.org/conference/nsdi20/presentation/zhang-peng 1:30 Lu et al. A Some Background on B...

    2020

  65. [1997]

    Des.10, 2/3 (1997), 171–206

    Algebraic Decision Diagrams and Their Applications.Formal Methods Syst. Des.10, 2/3 (1997), 171–206

    1997

  66. [2015]

    In12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15)

    A General Approach to Network Configuration Analysis. In12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15). USENIX Association, Oakland, CA, 469–483. https://www.usenix.org/conference/ nsdi15/technical-sessions/presentation/fogel

  67. [2024]

    InProceedings of the ACM SIGCOMM 2024 Conference(Sydney, NSW, Australia)(ACM SIGCOMM ’24)

    Alibaba HPN: A Data Center Network for Large Language Model Training. InProceedings of the ACM SIGCOMM 2024 Conference(Sydney, NSW, Australia)(ACM SIGCOMM ’24). Association for Computing Machinery, New York, NY, USA, 691–706. doi:10.1145/3651890.3672265

    arXiv 2024