BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:From Separation Logic to Systems Code - Peter O'Hearn - Queen Mary
  University of London
DTSTART:20100428T131500Z
DTEND:20100428T141500Z
UID:TALK23757@talks.cam.ac.uk
CONTACT:Mateja Jamnik
DESCRIPTION:Separation Logic is a member of an "exotic" branch of logic\, 
 known as substructural logic. In this talk I describe how you can go from 
 this exotic logic to a software tool for verifying selected integrity prop
 erties of low-level systems programs. Along the way\, I will also draw in 
 some concepts from artificial intelligence and philosophy of science that 
 significantly boost the level of automation.\n\nThis talk is based on join
 t work with Cristiano Calcagno\, Dino Distefano and Hongseok Yang on the S
 pace Invader program analyzer.\n
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR