9-9:05am: Opening remarks by co-chairs.
9:05-10:05am:
- Experiences with Protocol Description.
Pamela Zave (AT&T Laboratories--Research) - An Implementation of Meta-routing using Coq.
Vilius Naudziunas, Timothy G. Griffin (Computer Laboratory University of Cambridge)
10:05-10:30am: Coffee break.
10:30am-noon:
- Automating the Testing of OpenFlow Applications.
Marco Canini, Dejan Kostić. (EPFL), Jennifer Rexford (Princeton University), Daniele Venzano (EPFL) - Partial Specification of Routing Configurations.
Alexander J. T. Gurney (University of Pennsylvania), Limin Jia (CMU), Anduo Wang, Boon Thau Loo (University of Pennsylvania) - Toward a Lightweight Model of BGP Safety.
Matvey Arye, Rob Harrison, Richard Wang (Princeton University), Pamela Zave (AT&T Laboratories--Research),
Jennifer Rexford (Princeton University).
1:30-2:30pm:
- Modelling and Analysis of AODV in UPPAAL.
Ansgar Fehnker, Rob van Glabbeek, Peter Höfner (NICTA), Annabelle McIver (Macquarie University),
Marius Portmann, Wee Lum Tan (NICTA) - Absorbing Lexicographic Products in Metarouting.
Eric Parsonage, Hung X. Nguyen, Matthew Roughan (University of Adelaide, Australia).
3-4:15pm: Tool demonstrations by authors of accepted papers.
- Analyzing protocols with iSpin. Pamela Zave (AT&T Labs Research).
- An Implementation of Meta-routing using Coq. Timothy Griffin (Cambridge University).
- Automating the Testing of OpenFlow Applications. Canini Marco (EPFL).
- Model Checking AODV using UPPAAL. Peter Höfner (NICTA).
- Generalized Graph Products for Network Design and Analysis. Hung Nguyen, University of Adalaide, Australia)
4:15-4:30pm: Break
4:30-6pm: Panel discussion on Whither formal methods in Networking?.
- Participants: Ana Cavalli (TELECOM SudParis), Timothy Griffin (Cambridge University), Jonathan Sobel (Cisco), Pamela Zave (AT&T Labs Research).