BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Proving that programs eventually do something good - Byron Cook\, 
 Microsoft Research Cambridge
DTSTART:20120703T154500Z
DTEND:20120703T164500Z
UID:TALK38775@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Software failures can be sorted into two groups: those that ca
 use the software to do something wrong (e.g. crashing)\, and those that re
 sult in the software not doing something useful (e.g. hanging). In recent 
 years automatic tools have been developed which use mathematical proof tec
 hniques to certify that software cannot crash. But\, based on Alan Turing'
 s proof of the halting problem's undecidability\, many have considered the
  dream of automatically proving the absence of hangs to be impossible. Whi
 le not refuting Turing's original result\, recent research now makes this 
 dream a reality. This lecture will describe this recent work and its appli
 cation to industrial software.
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR