{"473281":{"#nid":"473281","#data":{"type":"event","title":"SCS Lecture - Network Verification and Synthesis - When Hoare Meets Cerf - Dr. George Varghese","body":[{"value":"\u003Cp class=\u0022p1\u0022\u003ETalk Topic:\u0026nbsp; Network Verification and Synthesis - When Hoare Meets Cerf\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003ESpeaker:\u0026nbsp; George Varghese, Ph.D. Principal Researcher and Partner at Microsoft Research\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003E\u003Cstrong\u003E\u003Cbr \/\u003E\u003C\/strong\u003E\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003E\u003Cstrong\u003EABSTRACT:\u0026nbsp;\u003C\/strong\u003E\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003ESurveys reveal that network outages are prevalent, and that many outages take hours to resolve, resulting in significant lost revenue. Many bugs are caused by errors in configuration files which are programmed using arcane, low-level languages, akin to machine code. Taking our cue from program and hardware verification, we suggest fresh approaches.\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003EI will first describe a geometric model of network forwarding called Header Space. While header space analysis is similar to finite state machine verification, we exploit domain-specific structure to scale better than off-the shelf model checkers.\u0026nbsp;\u0026nbsp; Next, I show how to exploit \u003Cem\u003Ephysical\u003C\/em\u003E symmetry to scale network verification for large data centers. While Emerson and Sistla showed how to exploit symmetry for model checking in 1996, they exploited symmetry on the \u003Cem\u003Elogical \u003C\/em\u003EKripke structure.\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003E\u0026nbsp;\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003EWhile the first part of the talk is about \u003Cem\u003Eanalysis\u003C\/em\u003E, I will then describe our work in synthesis.\u0026nbsp;\u0026nbsp; I will set the stage by describing a reconfigurable router architecture called RMT and an emerging language for programming routers called P4 that promises to extend the boundaries of Software Designed Networks. I will then describe two synthesis efforts for flexible routers, one akin to register allocation (table layout) and one akin to code generation (packet transactions).\u0026nbsp; (With collaborators at Edinburgh, MSR, MIT, Stanford, and University of Washington.)\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003E\u003Cbr \/\u003E\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003E\u003Cstrong\u003EBIO:\u003C\/strong\u003E\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003EGeorge Varghese received his Ph.D. in 1992 from MIT. From 1993-1999, he was a professor at Washington University, and at UCSD from 1999 to 2013. He was the Distinguished Visitor in the computer science department at Stanford University from 2010-2011. He joined Microsoft Research in 2012.\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003EHis book \u0022Network Algorithmics\u0022 was published in December 2004 by Morgan-Kaufman. In May 2004, he co-founded NetSift, which was acquired by Cisco Systems in 2005. With colleagues, he has won best paper awards at SIGCOMM (2014), ANCS (2013), OSDI (2008), PODC (1996), and the IETF Applied Networking Prize (2013). He won the Kobayashi Award and the SIGCOMM Lifetime Award, both in 2014, and the IIT Bombay Distinguished Alumni Award in 2015.\u0026nbsp;\u003C\/p\u003E","summary":null,"format":"limited_html"}],"field_subtitle":"","field_summary":"","field_summary_sentence":[{"value":"SCS Lecture Series - Network Verification and Synthesis - When Hoare Meets Cerf - Dr. George Varghese"}],"uid":"28150","created_gmt":"2015-11-24 16:04:35","changed_gmt":"2017-04-13 21:17:33","author":"Birney Robert","boilerplate_text":"","field_publication":"","field_article_url":"","field_event_time":{"event_time_start":"2015-12-03T15:00:00-05:00","event_time_end":"2015-12-03T16:00:00-05:00","event_time_end_last":"2015-12-03T16:00:00-05:00","gmt_time_start":"2015-12-03 20:00:00","gmt_time_end":"2015-12-03 21:00:00","gmt_time_end_last":"2015-12-03 21:00:00","rrule":null,"timezone":"America\/New_York"},"extras":[],"hg_media":{"473291":{"id":"473291","type":"image","title":"George Varghese","body":null,"created":"1449257190","gmt_created":"2015-12-04 19:26:30","changed":"1475895223","gmt_changed":"2016-10-08 02:53:43","alt":"George Varghese","file":{"fid":"203966","name":"gvheadshot.jpg","image_path":"\/sites\/default\/files\/images\/gvheadshot_0.jpg","image_full_path":"http:\/\/www.tlwarc.hg.gatech.edu\/\/sites\/default\/files\/images\/gvheadshot_0.jpg","mime":"image\/jpeg","size":654681,"path_740":"http:\/\/www.tlwarc.hg.gatech.edu\/sites\/default\/files\/styles\/740xx_scale\/public\/images\/gvheadshot_0.jpg?itok=Vzp06dAD"}}},"media_ids":["473291"],"groups":[{"id":"47223","name":"College of Computing"},{"id":"50875","name":"School of Computer Science"}],"categories":[],"keywords":[{"id":"654","name":"College of Computing"},{"id":"109","name":"Georgia Tech"},{"id":"166941","name":"School of Computer Science"}],"core_research_areas":[],"news_room_topics":[],"event_categories":[{"id":"1795","name":"Seminar\/Lecture\/Colloquium"}],"invited_audience":[{"id":"78751","name":"Undergraduate students"},{"id":"78761","name":"Faculty\/Staff"},{"id":"78771","name":"Public"},{"id":"174045","name":"Graduate students"}],"affiliations":[],"classification":[],"areas_of_expertise":[],"news_and_recent_appearances":[],"phone":[],"contact":[{"value":"\u003Cp\u003EJoy West\u003C\/p\u003E\u003Cp class=\u0022p1\u0022\u003E\u003Ca href=\u0022mailto:jwest62@cc.gatech.edu\u0022\u003Ejwest62@cc.gatech.edu\u003C\/a\u003E\u003C\/p\u003E","format":"limited_html"}],"email":[],"slides":[],"orientation":[],"userdata":""}}}