Date: April 18, 2017
Time: 1:30-2:30pm ET
Abstract
NetKAT is a formal system that can be used to program, model, and reason about networks. It comes with a rich formal toolkit including a sounds and complete algebraic axiomatization; an automata theory; a denotational semantics; and an efficient symbolic representation. These theoretic foundations enable powerful tools such as a decision procedure that allows fully automatic verification of important network properties; and a fast compiler that implements powerful programming abstractions. I will give a tutorial on NetKAT, showing how to use it to program networks and reason about their properties.
Bio
Steffen Smolka is a PhD student in Computer Science at Cornell University advised by Nate Foster. Currently his research focuses on languages, tools, and formal foundations for software defined networking. General areas of interest include (probabilistic) semantics, automata theory, and compilers.