Dexter Kozen præsenterer den nyeste forskning inden for NetKat
Fredag d. 13. marts holdt gæsteprofessor Dexter Kozen fra Cornell University foredrag om de nyeste gennembrud i udviklingen af NetKat, et højniveau sprog til at programmere netværk. Her kan du se hele foredraget på film.
Dexter Kozen gæster for øjeblikket DIKU i en periode på et halvt år for at forske i logik i programmeringssprog og arbejde sammen med DIKU-professor Fritz Henglein. I den anledning har han indvilliget i at give en DIKU Talk om sin forskning.
Billeder fra arrangementet
Dexter Kozen er netop blevet optaget som æresmedlem i Den europæiske forening for teoretisk datalogi (EATCS).
Læs abstract fra talken
NetKat: A Formal System for the Verification of Network
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.
In contrast to competing approaches, NetKAT has a formal mathematical semantics and an equational deductive system that is sound and complete over that semantics, as well as an efficient decision procedure. It is based on Kleene algebra with tests (KAT), an algebraic system for propositional program verification that has been extensively studied for nearly two decades. Several practical applications of NetKAT have been developed, including algorithms for testing reachability and non-interference and a correctness proof for a compiler that translates programs to hardware instructions for SDN switches.
In this talk I will present a survey of this recent work.