NetKAT: A Formal System for the Verification of Networks
ABSTRACT: Networks have received widespread attention in recent years as a target for domain-specific language design. The emergence of software-defined networking (SDN) as a popular paradigm for network programming has led to the appearance of a number of SDN programming languages that seek to provide high-level abstractions to simplify the task of specifying the packet-processing behavior of a network. Recent work by Anderson et al. (POPL 14) and Foster et al. (POPL 15) introduced NetKAT, a language and logic for reasoning about packet-switching networks. NetKAT provides general-purpose programming constructs such as parallel and sequential composition, conditional tests, and iteration, as well as special purpose primitives for querying and modifying packet headers and encoding network topologies.
BIO: Dexter Kozen is the Joseph Newton Pew, Jr. Professor in Engineering at Cornell University. He received his undergraduate degree from Dartmouth College in mathematics in 1974 and his PhD from Cornell in computer science in 1977. After working as a member of the research staff at the IBM Thomas J. Watson Research Center for several years, he returned to Ithaca to join the Cornell faculty in computer science in 1985. He is a former Guggenheim fellow and a fellow of the Association of Computing Machinery, the American Association for the Advancement of Science, and the European Association of Theoretical Computer Science. He is a recipient of the John G. Kemeny Prize in Computing, an IBM Outstanding Innovation Award, the 2016 EATCS Award, and the 2016 IEEE Computer Society McDowell Award. Kozen's research interests span a variety of topics on the boundary of computer science and mathematics: design and analysis of algorithms, computational complexity theory, complexity of decision problems in logic and algebra, and logics and semantics of programming languages. He is the author of over 150 research articles and four books.