BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Program Verification Using Cyclic Proof - Reuben Rowe\, UCL
DTSTART:20160519T120000Z
DTEND:20160519T130000Z
UID:TALK66041@talks.cam.ac.uk
CONTACT:Dominic Orchard
DESCRIPTION:I will talk about the work I have been doing extending the Cyc
 list automatic verification tool. I will first give an overview of the cyc
 lic proof technique\, which generalises infinite descent style proof-by-co
 ntradiction\, and explain how it can be used to prove entailments in both 
 first order logic\, and separation logic. I will then describe how it can 
 also be used in a Hoare-style system for proving the safety and terminatio
 n of heap-manipulating procedural programs\, and some of the technical cha
 llenges this involves. 
LOCATION:FW26
END:VEVENT
END:VCALENDAR