A coalgebraic decision procedure for NetKAT

Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, Laure Thompson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

65 Scopus citations

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. 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.

Original languageEnglish (US)
Title of host publicationPOPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PublisherAssociation for Computing Machinery
Pages343-355
Number of pages13
ISBN (Electronic)9781450333009
DOIs
StatePublished - Jan 14 2015
Externally publishedYes
Event42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015 - Mumbai, India
Duration: Jan 12 2015Jan 18 2015

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
Volume2015-January
ISSN (Print)0730-8566

Other

Other42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015
Country/TerritoryIndia
CityMumbai
Period1/12/151/18/15

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Automata
  • Brzozowski derivatives
  • Coalgebra
  • Kleene algebra with tests
  • NetKAT
  • Network verification

Fingerprint

Dive into the research topics of 'A coalgebraic decision procedure for NetKAT'. Together they form a unique fingerprint.

Cite this