Talk "NetKAT - a formal system for the verification of networks "

by Alexandra Silva

Sat, 27 June 2015 at 09:00 am in Nijmegen, The Netherlands

Joint work with: Nate Foster, Dexter Kozen, Matthew Milano, Laure Thompson

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. In our POPL 15 paper we developed the coalgebraic theory of NetKAT, including a specialized version of the Brzozowski derivative, and presented a new efficient algorithm for deciding the equational theory using bisimulation. In this talk I will present NetKAT and the main results concerning the language semantics and equivalence checking.