BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Mechanically Proving Hoare Formulae - Mike Gordon (University of C
 ambridge)
DTSTART:20090428T120000Z
DTEND:20090428T130000Z
UID:TALK17985@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:The Hoare formula P {Q} R had its 40th birthday this year! The
  ideas appearing in Hoare's 1969 paper are the basis for program verificat
 ion today\, but now they are mechanised inside complex and sophisticated v
 erification systems. I will compare automated methods for proving\nHoare f
 ormulae based both on the forward computation of postconditions and on the
  backwards computation of preconditions. Although precondition methods are
  better known\, I will argue the case for computing postconditions as this
  provides a verification spectrum ranging from symbolic execution (e.g. bo
 unded model checking) to full\nproof of correctness.\n\nMy talk is a revis
 ed and extended version of what I presented at the recent Tony Hoare 75 bi
 rthday celebration event. I have made a few corrections and added some det
 ails on the semantic encoding in HOL.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR