BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automatic termination proofs for software - Byron Cook\, Microsoft
  Research
DTSTART:20061115T141500Z
DTEND:20061115T151500Z
UID:TALK5372@talks.cam.ac.uk
CONTACT:Timothy G. Griffin
DESCRIPTION:I will describe recent advances in the area of automatic progr
 am\ntermination analysis. In particular\, I will describe the development 
 of\nseveral automatic tools\, called TERMINATOR and MUTANT\, which impleme
 nt\nnew termination analysis algorithms. These tools have been used to pro
 ve\nthat Windows device driver dispatch routines always return control bac
 k\nto their caller. The tools have also found a number of critical\ntermin
 ation bugs in device drivers.\n\n\nBio:\nDr. Byron Cook is a researcher at
  Microsoft Research\, Cambridge.   His\nresearch interests include automat
 ic formal software verification\,\nautomatic theorem proving\, and program
 ming language theory.  Before\ncoming to Cambridge Byron co-developed the 
 SLAM software model checker.\nSLAM is now used in a Windows product called
  Static Driver Verifier\,\nwhich automatically finds bugs in Windows OS de
 vice drivers. Before\njoining Microsoft\, Byron worked at Prover Technolog
 y. Byron's PhD is\nfrom OGI. For more information about Byron\, see\nhttp:
 //research.microsoft.com/~bycook.\n\n
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR