A Coalgebraic Decision Procedure for NetKAT

5 years 23 hour ago
A Coalgebraic Decision Procedure for NetKAT
Program 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 us...
Nate Foster, Dexter Kozen, Matthew Milano, Alexand
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where POPL
Authors Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva 0001, Laure Thompson
Comments (0)