Formal Foundations for Networks

In many fields of computing, techniques ranging from testing to formal modeling to full-blown verification have been successfully used to build reliable systems. But networks have largely resisted analysis using formal techniques. This talk will present recent work on developing a mathematical foundation for networks including a detailed operational model of software-defined networks, its formalization in the Coq proof assistant, a machine-verified compiler and run-time system for the NetCore programming language, and an automatic property-checking tool based on Z3.

Joint work with Arjun Guha, Mark Reitlbatt, and Rebecca Coombes. A forthcoming paper in the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) describes our system in further detail.

Speaker Bios

Nate Foster is an Assistant Professor of Computer Science at Cornell University. His research focuses on developing language abstractions and tools for building reliable systems. He received a PhD in Computer Science from the University of Pennsylvania in 2009, an MPhil in History and Philosophy of Science from Cambridge University in 2008, and a BA in Computer Science from Williams College in 2001. He was a postdoc at Princeton University from 2009-2010. His awards include an NSF CAREER award, a Sloan Research Fellowship, a Yahoo! Academic Career Enhancement Award, and the Morris and Dorothy Rubinoff Award.

Date:
Haut-parleurs:
Nate Foster
Affiliation:
Cornell University