@inproceedings{2dac12b996204cd99cd7aaa5199fedfb,
title = "An Algebraic Approach to Automatic Reasoning for NetKAT Based on Its Operational Semantics",
abstract = "NetKAT is a network programming language with a solid mathematical foundation. In this paper, we present an operational semantics and show that it is sound and complete with respect to its original axiomatic semantics. We achieve automatic reasoning for NetKAT such as reachability analysis and model checking of temporal properties, by formalizing the operational semantics in an algebraic executable specification language called Maude. In addition, as NetKAT policies are normalizable, two policies are operationally equivalent if and only if they can be converted into the same normal form. We provide a formal way of reasoning about network properties by turning the equivalence checking problem of NetKAT policies into the normalization problem that can be automated in Maude.",
keywords = "LTL, Maude, Model checking, NetKAT, Operational semantics",
author = "Yuxin Deng and Min Zhang and Guoqing Lei",
note = "Publisher Copyright: {\textcopyright} 2017, Springer International Publishing AG.; 19th International Conference on Formal Engineering Methods, ICFEM 2017 ; Conference date: 13-11-2017 Through 17-11-2017",
year = "2017",
doi = "10.1007/978-3-319-68690-5\_28",
language = "英语",
isbn = "9783319686899",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "464--480",
editor = "Zhenhua Duan and Luke Ong",
booktitle = "Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Proceedings",
address = "德国",
}