NetKAT: A FORMAL SYSTEM FOR THE VERIFICATION OF NETWORKS

Add to your list(s) Download to your calendar using vCal

• Alexandra Silva (UCL)
• Friday 15 January 2016, 11:00-12:00
• CS 217.

If you have a question about this talk, please contact Neel Krishnaswami.

NetKAT is a relatively new programming language and logic for reasoning about packet switching networks that fits well with the popular software defined networking (SDN) paradigm. NetKAT was introduced quite recently by Anderson et al. (POPL 2014) and further developed by Foster et al. (POPL 2015). The system 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. The language allows the desired behavior of a network to be specified equationally. It has a formal categorical semantics and a deductive system that is sound and complete over that semantics, as well as an efficient decision procedure for the automatic verification of equationally-defined properties of networks.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• CS 217
• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.