BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY: Local Reasoning for Storable Locks and Threads - Alexey Gotsman (
 University of Cambridge)
DTSTART:20070515T120000Z
DTEND:20070515T130000Z
UID:TALK7411@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:We present a resource-oriented program logic that is able to r
 eason about concurrent heap-manipulating programs with unbounded numbers o
 f dynamically-allocated locks and threads. The logic is inspired by concur
 rent separation logic\, but handles these more realistic concurrency primi
 tives. We demonstrate that the proposed logic allows for local reasoning a
 bout programs that exhibit a high degree of information hiding in their lo
 cking mechanisms. This is joint work with Josh Berdine\, Byron Cook (MSR)\
 , Noam Rinetzky\, Mooly Sagiv (Tel-Aviv University).
LOCATION:Computer Laboratory\, William Gates Building\, Room GS15
END:VEVENT
END:VCALENDAR