A Coalgebraic Decision Procedure for NetKAT
Abstract
NetKAT is a domain-specific language and logic for specifying and verifying network packet-processing functions. It consists of Kleene algebra with tests (KAT) augmented with primitives for testing and modifying packet headers and encoding network topologies. Previous work developed the design of the language and its standard semantics, proved the soundness and completeness of the logic, defined a PSPACE algorithm for deciding equivalence, and presented several practical applications.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 14, 2015
- Source ID
- 10.1145/2775051.2677011
Entities
People
- Alexandra Silva
- Dexter Kozen
- Laure Thompson
- Mae Milano
- Nate Foster
Organizations
- Cornell University
- National Science Foundation
- Office of Naval Research
- Radboud University Nijmegen