BEGIN:VCALENDAR
METHOD:PUBLISH
VERSION:2.0
PRODID:-//Cornell U. Department of Computer Science//Brown Bag Seminar//EN
BEGIN:VEVENT
SUMMARY:Brown bag: Nate Foster
DESCRIPTION:Title: Verifying Network Data Planes\nSpeaker: Nate
	 Foster\nAbstract: P4 is a new language for programming network data
	 planes. The language provides domain-specific constructs for describing
	 the input-output formats and functionality of packet-processing
	 pipelines. Unfortunately P4 programs can go wrong in a variety of
	 interesting and frustrating ways including reading uninitialized data\,
	 generating malformed packets\, and failing to handle exceptions. In this
	 talk\, I will present the design and implementation of p4v\, a tool for
	 verifying P4 programs. The tool is based on classic software
	 verification techniques (due to Hoare\, Dijkstra\, Flanagan\, Leino\,
	 etc.)\, but adds several important innovations: a novel mechanism for
	 incorporating control-plane assumptions and domain-specific
	 optimizations\, both of which are needed to scale up to large programs.
	 I will discuss our experiences applying p4v to a variety of real-world
	 programs including switch.p4\, a large program that implements the
	 functionality of a conventional switch.\n\np4v is joint work with Bill
	 Hallahan (Yale)\, JK Lee (Barefoot)\, Cole Schlesinger (Barefoot)\,
	 Steffen Smolka (Cornell)\, Robert Soule (Barefoot and USI)\, and Han
	 Wang (Barefoot).
LOCATION:Gates 122
UID:2017-09-26
STATUS:CONFIRMED
DTSTART:20170926T160000Z
DTEND:20170926T170000Z
LAST-MODIFIED:20170922T143622Z
ORGANIZER;CN=Jonathan Shi:http://www.cs.cornell.edu/~jshi/brownbag/
DTSTAMP:20260408T173041Z
END:VEVENT
END:VCALENDAR