BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/838
DTSTAMP:20230914T125940Z
SUMMARY:Network Verification -- When Clarke Meets Cerf
DESCRIPTION:Speaker: George Varghese (University of California Los Angeles\
 nDepartment of Computer Science\n4531C Boulter Hall\nCA 90095\nUnited Stat
 es of America)\n\nAbstract: \nSurveys reveal that network outages are prev
 alent\, and that many outages take hours to resolve\, resulting in signifi
 cant lost revenue. Many bugs are caused by errors in configuration files w
 hich are programmed using arcane\, low-level languages\, akin to machine c
 ode. Taking our cue from program and hardware verification\, we suggest fr
 esh approaches.\nI will first describe a geometric model of network forwar
 ding called Header Space. While header space analysis is similar to finite
  state machine verification\, we exploit domain-specific structure to scal
 e better than off-the shelf model checkers. Next\, I show how to exploit p
 hysical symmetry to scale network verification for large data centers. Whi
 le Emerson and Sistla showed how to exploit symmetry for model checking in
  1996\, they exploited symmetry on the logical Kripke structure.\nWhile he
 ader space models allow us to verify the forwarding tables in routers\, th
 ere are also routing protocols such as BGP that build the forwarding table
 s.  We show to go from headerspace verification to what we call control s
 pace verification to proactively catch latent bugs in BGP configurations.
   I will end\nwith a vision for what we call Network Design Automation to
  build a suite of tools for networks inspired by the Electronic Design Aut
 omation Industry.\n(With collaborators at CMU\, Edinburgh\, MSR\, Stanford
 \, and UCLA.)\n
URL:https://www.tcs.tifr.res.in/web/events/838
DTSTART;TZID=Asia/Kolkata:20171228T160000
DTEND;TZID=Asia/Kolkata:20171228T170000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR