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:20100217T141500Z
DTEND:20100217T151500Z
UID:TALK22088@talks.cam.ac.uk
CONTACT:Mateja Jamnik
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.  Based on Alan Turing's pro
 of of the halting problem's undecidablity\, many have considered the dream
  of automatically proving the absence of hangs to be impossible. While not
  refuting Turing's original result\, recent research now makes this dream 
 a reality. This lecture will describe this recent work and its application
  to industrial software.\n
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR