Weighted NetKAT: A Programming Language For Quantitative Network Verification

Emmanuel Suárez Acevedo; Tiago Ferreira; Kevin Batz; Oliver Bøving; Nate Foster; Alexandra Silva

Home/Archive/arXiv

arXiv · 2604.13987

Weighted NetKAT: A Programming Language For Quantitative Network Verification

Emmanuel Suárez Acevedo·Tiago Ferreira·Kevin Batz·Oliver Bøving·Nate Foster·Alexandra Silva

View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.PL

Keep this discovery

BibTeX RIS

Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Bøving, Nate Foster, Alexandra Silva. 2026-09-01. Weighted NetKAT: A Programming Language For Quantitative Network Verification. https://arxiv.org/abs/2604.13987

Cite the original work for its findings. Save a collection to share your selection of sources.

Discover connections

cs.PL subject

Connections use source metadata and explicit phrase matches, not verified experimental comparisons.

KEEP EXPLORING

Related papers

arXiv2026

URIUM: A Programming Language for a Practical Open Course on Compiler Design

This paper presents the definition of a simple programming language used as the basis for developing a practical compiler design course. The course explains step by step how to build a compiler, from the initial analysis stages to code generation. The developed compiler generates code for various processors (MIPS, Intel, and RISC-V) and operating systems (MS-Windows and Linux). The course can be adapted to different levels of difficulty and can be used as a starting point for explaining more advanced topics.

cs.PL↗

arXiv2026

Beyond Locks and Thread IDs: Static Data Race Detection Off The Beaten Path (Extended Version)

Maintaining an abstraction of the execution history of threads can improve the precision of data race detection in static analysis. Here, we extend the digest framework to handle concurrency constructs and synchronization mechanisms that have been ignored in static race detection. We introduce mechanisms for the commonly used thread barriers, as well as pthread_once, which allows to ensure that an action is executed only once. We also instantiate the framework with an abstraction of locksets held by ancestor threads. We propose a suite of litmus tests to evaluate analyses for these features and compare our implementation to state-of-the-art tools, finding that they lack support.

cs.PL↗

arXiv2026

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT

This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate applicability of our algorithms, we designed symbolic derivatives for CF-GKAT, a practical system based on GKAT designed to validate control-flow transformations. We implemented the algorithms in Rust and evaluated them on both randomly generated benchmarks and real-world control-flow transformations. Indeed, we observed order-of-magnitude performance improvements against existing implementations for both KAT and CF-GKAT. Notably, our experiments also revealed a bug in Ghidra, an industry-standard decompiler, highlighting the practical viability of these systems.

cs.PL↗