BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A rigorous approach to networking: TCP\, from implementation to pr
 otocol to service - Tom Ridge (University of Cambridge)
DTSTART:20080212T130000Z
DTEND:20080212T140000Z
UID:TALK9884@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Speaker: Tom Ridge\n\nDespite more then 30 years of research o
 n protocol specification\, the major protocols deployed in the Internet\, 
 such as TCP\, are described only in informal prose RFCs and executable cod
 e. In part this is because the scale and complexity of these protocols mak
 es them challenging targets for formalization.\n\nIn this work we show how
  these difficulties can be addressed. We develop a high-level specificatio
 n for TCP and the Sockets API\, expressed in the HOL proof assistant\, des
 cribing the byte-stream service that TCP provides to users.  This compleme
 nts our previous low-level specification of the protocol internals\, and m
 akes it possible for the first time to state what it means for TCP to be c
 orrect: that the protocol implements the service. We define a precise abst
 raction function between the models and validate it by testing\, using ver
 ified testing infrastructure within HOL. This is a pragmatic alternative t
 o full proof\, providing reasonable\nconfidence at a relatively low entry 
 cost.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR