A coalgebraic decision procedure for NetKAT

DOI10.1145/2676726.2677011MaRDI QIDQ2819821zbMATH OpenOpenAlexFDO

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

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

automataBrzozowski derivativescoalgebraKleene algebra with testsNetKATnetwork verification

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)

Recommendations

• A coalgebraic decision procedure for WS1S
• scientific article; zbMATH DE number 139614
• scientific article; zbMATH DE number 1497882
• A constructive denotational semantics for Kahn networks in Coq
• On logics for coalgebraic simulation
• An efficient Coq tactic for deciding Kleene algebras
• A coalgebraic semantics for causality in Petri nets
• A network-conscious \(\pi\)-calculus and its coalgebraic semantics
• Coalgebraic derivations in logic programming
• Coalgebraic logic programming: from Semantics to Implementation

Cited in

(24)

• Towards an analysis of dynamic gossip in Net\textsc{kat}
• Verified iptables firewall analysis and verification
• Actor-based model checking for software-defined networks
• Explaining safety failures in NetKAT
• Some complexity results for stateful network verification
• Completeness and incompleteness in nominal Kleene algebra
• Probabilistic NetKAT
• A fast compiler for NetKAT
• Nominal Kleene coalgebra
• scientific article; zbMATH DE number 139614 (Why is no real title available?)
• Undecidable Problems for Probabilistic Network Programming
• Netkat, semantic foundations for networks
• Kleene algebra with observations
• Local completeness logic on Kleene algebra with tests
• Concurrent NetKAT. Modeling and analyzing stateful, concurrent networks
• DyNetKAT: an algebra of dynamic networks
• A complete inference system for skip-free guarded Kleene algebra with tests
• Kleene theorems for lasso languages and -languages
• On star expressions and completeness theorems
• Guarded Kleene algebra with tests: automata learning
• A contextual formalization of structural coinduction
• Well-behaved (co)algebraic semantics of regular expressions in Dafny
• Guarded Kleene algebra with tests: coequations, coinduction, and completeness
• Kleene algebra with commutativity conditions is undecidable

This page was built for publication: A coalgebraic decision procedure for NetKAT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819821)