99 citations · 382 across the 19 of their papers we have counts for
13 papers · 1 filter
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…
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…
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…
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…
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…
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…