Show simple item record

dc.contributor.authorFoster, Nate
dc.contributor.authorKozen, Dexter
dc.contributor.authorMilano, Matthew
dc.contributor.authorSilva, Alexandra
dc.contributor.authorThompson, Laure
dc.date.accessioned2014-03-26T23:18:03Z
dc.date.available2014-03-26T23:18:03Z
dc.date.issued2014-03-26
dc.identifier.urihttps://hdl.handle.net/1813/36255
dc.description.abstractProgram equivalence is a fundamental problem that has practical applications across a variety of areas of computing including compilation, optimization, software synthesis, formal verification, and many others. Equivalence is undecidable in general, but in certain settings it is possible to develop domain-specific languages that are expressive enough to be practical and yet sufficiently restricted so that equivalence remains decidable. In previous work we introduced NetKAT, a domain-specific language for specifying and verifying network packet-processing functions. NetKAT provides familiar constructs such as tests, assignments, union, sequential composition, and iteration as well as custom primitives for modifying packet headers and encoding network topologies. Semantically, NetKAT is based on Kleene algebra with tests (KAT) and comes equipped with a sound and complete equational theory. Although NetKAT equivalence is decidable, the best known algorithm is hardly practical-it uses Savitch's theorem to determinize a PSPACE algorithm and requires quadratic space. This paper presents a new algorithm for deciding NetKAT equivalence. This algorithm is based on finding bisimulations between finite automata constructed from NetKAT programs. We investigate the coalgebraic theory of NetKAT, generalize the notion of Brzozowski derivatives to NetKAT, develop efficient representations of NetKAT automata in terms of spines and sparse matrices, and discuss the highlights of our prototype implementation.en_US
dc.language.isoen_USen_US
dc.subjectNetKATen_US
dc.subjectKleene algebraen_US
dc.subjectKleene algebra with testsen_US
dc.subjectBrzozowski derivativeen_US
dc.subjectSoftware-defined networksen_US
dc.titleA Coalgebraic Decision Procedure for NetKATen_US
dc.typetechnical reporten_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

Statistics