[talks] Ryan Beckett will be presenting his Generals on May 15, 2015 at 2:30pm in CS 401.

[Nicki Gotsis]

Ryan Beckett will be presenting his Generals on May 15, 2015 at 2:30pm in CS 401.

The members of his committee are as follows: David Walker (advisor), Aarti Gupta, and Andrew Appel.

Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so.  His abstract and reading list follow below.

Abstract:
Kleene algebra with tests (KAT) is a well-studied algebraic structure consisting of a Kleene
Algebra with an embedded Boolean subalgebra. KAT has been applied to a wide variety of equational
program specification and verification tasks including communication protocols, static program
analysis, lazy caching, concurrency control, and compiler optimizations. NetKAT, a KAT for defining
network policies, has recently garnered much attention for its utility in both programming networks
and verifying network program equivalence.

We formalize an algebraic extension to NetKAT by lifting its Boolean subalgebra to a more expressive
past-time linear temporal logic with tests ranging over packet history. Temporal logic tests enable
the modular specification of networking properties such as reachability and waypointing,
the construction of queries for network monitoring and debugging, and the concise description of programs
using history-based routing. We develop an equational theory for NetKAT with an embedded temporal logic
and prove that the equational theory is both sound and complete with respect to the denotational semantics.
We conclude by discussing the broader applicability of our approach to KAT in general.

Books:

 B. Pierce, Types and programming languages. MIT Press, 2002. (chapters 1-17, 20-25)
 M. Huth and M. Ryan, Logic in computer science, 2nd ed. Cambridge University Press, 2000. (chapters 1-5)
 D. Harel, D. Kozen and J. Tiuryn, Dynamic logic. MIT Press, 2000. (chapter 5)

Papers:

 R. Jhala and R. Majumdar. Software model checking. ACM Comput. Surv., 41(4):1–54, 2009.
 L. Zhang and S. Malik. The quest for efficient boolean satisfiability solvers. In CAV, 2002.
 J. Desharnais, B. Moller and G. Struth. Modal Kleene algebra and applications: a survey. Relational Methods in Computer Science, 1:93–131, 2004.
 A. Greenburg et al. A clean slate 4D approach to network control and management. In SIGCOMM, 2005.
 P. Kazemian, G. Varghese and N. McKeown. Header space analysis: static checking for networks. In NSDI, 2012.
 S. Basu et al. Merlin: a language for provisioning network resources. In CoNEXT, 2014.
 C. Monsanto et al. A compiler and run-time system for network programming languages. In POPL, 2012.
 C. Anderson et al. NetKAT: semantic foundations for networks. In POPL, 2014.
 N. Foster et al. A coalgebraic decision procedure for NetKAT. In POPL, 2015.