TY - GEN
T1 - A coalgebraic decision procedure for NetKAT
AU - Foster, Nate
AU - Kozen, Dexter
AU - Milano, Matthew
AU - Silva, Alexandra
AU - Thompson, Laure
N1 - Publisher Copyright:
Copyright © 2015 by the Association for Computing Machinery, Inc. (ACM).
PY - 2015/1/14
Y1 - 2015/1/14
N2 - 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. This paper develops the coalgebraic theory of NetKAT, including a specialized version of the Brzozowski derivative, and presents a new efficient algorithm for deciding the equational theory using bisimulation. The coalgebraic structure admits an efficient sparse representation that results in a significant reduction in the size of the state space. We discuss the details of our implementation and optimizations that exploit NetKAT's equational axioms and coalgebraic structure to yield significantly improved performance. We present results from experiments demonstrating that our tool is competitive with state-of-the-art tools on several benchmarks including allpairs connectivity, loop-freedom, and translation validation.
AB - 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. This paper develops the coalgebraic theory of NetKAT, including a specialized version of the Brzozowski derivative, and presents a new efficient algorithm for deciding the equational theory using bisimulation. The coalgebraic structure admits an efficient sparse representation that results in a significant reduction in the size of the state space. We discuss the details of our implementation and optimizations that exploit NetKAT's equational axioms and coalgebraic structure to yield significantly improved performance. We present results from experiments demonstrating that our tool is competitive with state-of-the-art tools on several benchmarks including allpairs connectivity, loop-freedom, and translation validation.
KW - Automata
KW - Brzozowski derivatives
KW - Coalgebra
KW - Kleene algebra with tests
KW - NetKAT
KW - Network verification
UR - http://www.scopus.com/inward/record.url?scp=84939537312&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84939537312&partnerID=8YFLogxK
U2 - 10.1145/2676726.2677011
DO - 10.1145/2676726.2677011
M3 - Conference contribution
AN - SCOPUS:84939537312
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 343
EP - 355
BT - POPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PB - Association for Computing Machinery
T2 - 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015
Y2 - 12 January 2015 through 18 January 2015
ER -