Summer School on Formal Methods and Networks
June 10-14, 2013
Cornell University
Ithaca, NY, USA
Introduction
In many areas of computing, techniques ranging from testing to formal modeling to full-blown verification have been successfully used to help programmers create reliable systems. For example, in processor development, automated theorem proving uncovers deep bugs in designs before they become costly errors in silicon; avionics developers use program analysis to verify critical safety properties of the embedded software running on airplanes; and operating system vendors have successfully used model checking to eliminate entire classes of bugs in device drivers. But, until recently, networks have largely resisted analysis using formal techniques.
The goal of this summer school is to bring together leading researchers, graduate students, and industrial practitioners to study recent research results on applying formal methods to networks. The curriculum will consist of a series of lectures on topics from theoretical frameworks for modeling network behavior to practical techniques and tools. The lectures will be designed to be accessible to a general computer science audience and will not assume advanced knowledge of formal methods or networks.
Speakers
Nikolaj Bjorner
Microsoft Research
Satisfiability Modulo Theories Solving for Network Verification
Ahmed Khurshid and Brighten Godfrey
University of Illinois at Urbana-Champaign
Verifying Networks in Real Time
Timothy Griffin
University of Cambridge
Partial Automation in the Design and Implementation of Path-finding Algorithms
Arjun Guha
University of Massachusetts Amherst
Network Programming With Frenetic
Peyman Kazemian and Nick McKeown
Stanford University
Network Verification Using Header Space Analysis
Shriram Krishnamurthi and Tim Nelson
Brown University and Worcester Polytechnic Institute
Modeling and Reasoning about Network Components
Ratul Mahajan
Microsoft Research
Systematically Exploring the Behavior of Control Programs
Pamela Zave
AT&T Research
Compositional Abstractions of Network Architectures
Schedule
Monday, June 10th
- 03:00pm-03:30pm: Welcome
- David Walker, Jennifer Rexford, Nate Foster
- 03:30pm-05:30pm: Introduction to Frenetic
- Arjun Guha [notes]
Tuesday, June 11th
- 09:00am-10:30am: How to Make Chord Correct
- Pamela Zave [slides | code]
- 10:30am-11:00am: Break
- 11:00am-11:30am: Aluminum
- Shriram Krishnamurthi and Tim Nelson
- 11:30am-12:30pm: Forwarding Plane Correctness
- Nick McKeown [slides]
- 12:30pm-02:00pm: Lunch
- 02:00pm-03:30pm: Offline Data Plane Checking with Anteater and Header Space Analysis
- Brighten Godfrey and Peyman Kazemian [slides i | slides ii]
- 03:30pm-04:00pm: Break
- 04:00pm-06:00pm: Margrave
- Shriram Krishnamurthi and Tim Nelson [notes]
Wednesday, June 12th
Thursday, June 13th
- 09:00am-10:30am: The Geomorphic View of Networking
- Pamela Zave [slides]
- 10:30am-11:00am: Break
- 11:00am-11:45am: SMT II
- Nikolaj Bjorner [slides | examples]
- 11:45am-12:30pm: Metarouting II
- Timothy Griffin [slides]
- 12:30pm-02:00pm: Lunch
- 02:00pm-09:00pm: Excursion
Friday, June 14th
Registration
Application
Prospective applicants should complete the application form and ask their academic advisor or supervisor to send a brief letter justifying their participation to summerschool-application@lists.frenetic-lang.org. The letter should also specify the amount of funding available from the advisor or university for students who have applied for a scholarship. We will process applications and scholarship requests on a rolling basis and send notifications by email. The final application deadline is May 10th, 2013.
The fee for participating in the summer school is $160 for students and $240 for all others. This includes all registration costs, materials, and meals, as well as an outing on Wednesday afternoon. Dorm housing from June 10th through June 14th is available for an additional $200 (double) or $280 (single). Alternatively, participants may arrange their own housing. The Visit Ithaca website maintains a list of accommodations in the Ithaca area.
Scholarships
Generous support for the summer
school is provided by the National Science Foundation under grants
CNS-1111698 and CNS-1111520. To encourage broad participation, we
will offer scholarships to selected students.
Local Information
Registration and lectures will be held at the Robert
Purcell Community Center. Students will be housed in single and
double rooms in Mews
Hall. Both buildings are located on the north campus of Cornell
University. The following maps show the locations of Purcell and Mews.
Students should plan to arrive during the day on Monday, June 10th and depart after lunch on Friday, June 14th or anytime on Saturday, June 15th. Note that due to Cornell reunions, dorm rooms will not be available the night of Sunday, June 9th.
Ithaca's Tompkins Regional Airport has direct flights to Detroit, Newark, and Philadelphia. To book, use the airport code ITH. Cornell also runs a motor coach with daily service to and from New York City. See here for additional information on transportation options to Ithaca.
Resources
The following resources may be of interest to summer school attendees.
Organizers
Nate Foster (Cornell University)
Jennifer Rexford (Princeton University)
David Walker (Princeton University)