We provide a model of the language based on partially ordered multisets, well-established mathematical structures in the denotational semantics of concurrent languages. We prove that CNetKAT is a sound
and complete axiomatization of this model, and we illustrate the use of CNetKAT through various examples. More generally, CNetKAT is analgebraic framework to reason about programs with both local and
global state. In our model these are, respectively, the packets and the global variable store, but the scope of applications is much more general, including reasoning about hardware pipelines inside an SDN
switch. This is joint work with Jana Wagemaker, Nate Foster, Tobia Kappe, Dexter Kozen, and Jurriaan Rot.
Please contact the office team for link information,