BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verifying Distributed Systems: the Operational Approach - Tom Ridg
 e (University of Cambridge)
DTSTART:20090210T130000Z
DTEND:20090210T140000Z
UID:TALK16355@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:I will give an extended version of my recent POPL talk. The ab
 stract\nfor the POPL paper is as follows:\n\nThis work develops an integra
 ted approach to the verification of\nbehaviourally rich programs\, founded
  directly on operational\nsemantics.  The power of the approach is demonst
 rated with a\nstate-of-the-art verification of a core piece of distributed
 \ninfrastructure\, involving networking\, a filesystem\, and\nconcurrent O
 Caml code. The formalization is in higher-order\nlogic and proof support i
 s provided by the HOL4 theorem prover.\n\nDifficult verification problems 
 demand a wide range of techniques.\nHere these include ground and symbolic
  evaluation\, local reasoning\,\nseparation\, invariants\, Hoare-style ass
 ertional reasoning\,\nrely/guarantee\, inductive reasoning about protocol 
 correctness\,\nmultiple refinement\, and linearizability.  While each of t
 hese\ntechniques is useful in isolation\, they are even more so in combina
 tion. The first contribution of this paper is to present the operational a
 pproach and describe how existing techniques\,\nincluding all those mentio
 ned above\, may be cleanly and precisely\nintegrated in this setting.\n\nT
 he second contribution is to show how to combine verifications of\nindivid
 ual library functions with arbitrary and unknown user code in\na compositi
 onal manner\, focusing on the problems of private state\nand encapsulation
 .\n\nThe third contribution is the example verification itself. The\ninfra
 structure must behave correctly under arbitrary patterns of\nhost and netw
 ork failure\, whilst for performance reasons the code\nalso includes data 
 races on shared state. Both features make the\nverification particularly c
 hallenging.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR