A Coalgebraic Decision Procedure for NetKAT

DOI10.1145/2676726.2677011zbMath1346.68132OpenAlexW2151517515MaRDI QIDQ2819821

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

Publication date: 29 September 2016

Published in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2676726.2677011

zbMATH Keywords

coalgebraautomataKleene algebra with testsnetwork verificationBrzozowski derivativesNetKAT

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (12)

Nominal Kleene Coalgebra ⋮ Verified iptables firewall analysis and verification ⋮ Completeness and incompleteness in nominal Kleene algebra ⋮ Local completeness logic on Kleene algebra with tests ⋮ Concurrent NetKAT. Modeling and analyzing stateful, concurrent networks ⋮ Unnamed Item ⋮ DyNetKAT: an algebra of dynamic networks ⋮ Actor-based model checking for software-defined networks ⋮ Probabilistic NetKAT ⋮ Explaining safety failures in NetKAT ⋮ Undecidable Problems for Probabilistic Network Programming ⋮ Some complexity results for stateful network verification

This page was built for publication: A Coalgebraic Decision Procedure for NetKAT