alt text 

Stanford University Networking Seminar


Nate Foster (Cornell University)
Formal Foundations for Networks

12:00pm, Thursday April 18, 2013
Gates 104

About the Talk

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 detail http://www.cs.cornell.edu/~jnfoster/papers/frenetic-verified-controllers.pdf; an extended abstract will be presented at the Open Networking Summit http://www.cs.cornell.edu/~jnfoster/papers/frenetic-verified-controllers-ons.pdf.

About the Speaker

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