99 citations · 382 across the 19 of their papers we have counts for
22 papers
P4Testgen: An Extensible Test Oracle For P4
Fabian Ruffy, Jed Liu, Prathima Kotikalapudi +7
We present P4Testgen, a test oracle for the P4 language. P4Testgen supports automatic test generation for any P4 target and is designed to be extensible to many P4 targets.…
Formal Abstractions for Packet Scheduling
Anshuman Mohan, Yunhe Liu, Nate Foster +2
Early programming models for software-defined networking (SDN) focused on basic features for controlling network-wide forwarding paths, but more recent work has considered richer f…
Dependently-Typed Data Plane Programming
Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs +2
Programming languages like P4 enable specifying the behavior of network data planes in software. However, with increasingly powerful and complex applications running in the network…
Leapfrog: Certified Equivalence for Protocol Parsers
Ryan Doenges, Tobias Kappé, John Sarracino +2
We present Leapfrog, a Coq-based framework for verifying equivalence of network protocol parsers. Our approach is based on an automata model of P4 parsers, and an algorithm for sym…
Concurrent NetKAT: Modeling and analyzing stateful, concurrent networks
Jana Wagemaker, Nate Foster, Tobias Kappé +3
We introduce Concurrent NetKAT (CNetKAT), an extension of NetKAT with operators for specifying and reasoning about concurrency in scenarios where multiple packets interact through…
Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista +7
P4 is a domain-specific language for programming and specifying packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-acti…
TxForest: A DSL for Concurrent Filestores
Jonathan DiLorenzo, Katie Mancini, Kathleen Fisher +1
Many systems use ad hoc collections of files and directories to store persistent data. For consumers of this data, the process of properly parsing, using, and updating these filest…
Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time
Steffen Smolka, Nate Foster, Justin Hsu +3
Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union () and iteration () operations from KAT to pre…
How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4
Matthias Eichholz, Eric Campbell, Nate Foster +2
The P4 programming language offers high-level, declarative abstractions that bring the flexibility of software to the domain of networking. Unfortunately, the main abstraction used…
Scalable Verification of Probabilistic Networks
Steffen Smolka, Praveen Kumar, David M Kahn +4
This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probab…
NetChain: Scale-Free Sub-RTT Coordination (Extended Version)
Xin Jin, Xiaozhou Li, Haoyu Zhang +5
Coordination services are a fundamental building block of modern cloud systems, providing critical functionalities like configuration management and distributed locking. The major…
Probabilistic Program Equivalence for NetKAT
Steffen Smolka, Praveen Kumar, Nate Foster +4
We tackle the problem of deciding whether two probabilistic programs are equivalent in Probabilistic NetKAT, a formal language for specifying and reasoning about the behavior of pa…
Optimal Consistent Network Updates in Polynomial Time
Pavol Cerny, Nate Foster, Nilesh Jagnik +1
Software-defined networking (SDN) allows operators to control the behavior of a network by programatically managing the forwarding rules installed on switches. However, as is commo…
Cantor meets Scott: Semantic Foundations for Probabilistic Networks
Steffen Smolka, Praveen Kumar, Nate Foster +2
ProbNetKAT is a probabilistic extension of NetKAT with a denotational semantics based on Markov kernels. The language is expressive enough to generate continuous distributions, whi…
Kulfi: Robust Traffic Engineering Using Semi-Oblivious Routing
Praveen Kumar, Yang Yuan, Chris Yu +3
Wide-area network traffic engineering enables network operators to reduce congestion and improve utilization by balancing load across multiple paths. Current approaches to traffic…
Morpheus: Safe and Flexible Dynamic Updates for SDNs
Karla Saur, Joseph Collard, Nate Foster +3
SDN controllers must be periodically modified to add features, improve performance, and fix bugs, but current techniques for implementing dynamic updates are inadequate. Simply hal…
Event-Driven Network Programming
Jedidiah McClurg, Hossein Hojjat, Nate Foster +1
Software-defined networking (SDN) programs must simultaneously describe static forwarding behavior and dynamic updates in response to events. Event-driven updates are critical to g…
A Fast Compiler for NetKAT
Steffen Smolka, Spiridon Eliopoulos, Nate Foster +1
High-level programming languages play a key role in a growing number of networking platforms, streamlining application development and enabling precise formal reasoning about netwo…
Merlin: A Language for Provisioning Network Resources
Robert Soulé, Shrutarshi Basu, Parisa Jalili Marandi +4
This paper presents Merlin, a new framework for managing resources in software-defined networks. With Merlin, administrators express high-level policies using programs in a declara…
Toward Synthesis of Network Updates
Andrew Noyes, Todd Warszawski, Pavol Černý +1
Updates to network configurations are notoriously difficult to implement correctly. Even if the old and new configurations are correct, the update process can introduce transient e…
Efficient Synthesis of Network Updates
Jedidiah McClurg, Hossein Hojjat, Pavol Cerny +1
Software-defined networking (SDN) is revolutionizing the networking industry, but current SDN programming platforms do not provide automated mechanisms for updating global configur…
The Homeostasis Protocol: Avoiding Transaction Coordination Through Program Analysis
Sudip Roy, Lucja Kot, Gabriel Bender +5
Datastores today rely on distribution and replication to achieve improved performance and fault-tolerance. But correctness of many applications depends on strong consistency proper…