BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Concurrent abstract predicates - Mike Dodds
DTSTART:20100823T114500Z
DTEND:20100823T130000Z
UID:TALK25439@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Abstraction is key to understanding and reasoning about large 
 computer systems. Abstraction is simple to achieve if data structures are 
 disjoint\, but rather difficult when they are partially shared\, as is oft
 en the case for concurrent modules. In this talk I will present a program 
 logic for reasoning abstractly about data structures that provides a ficti
 on of disjointness and permits compositional reasoning. The internal detai
 ls of a module are completely hidden from the client by concurrent abstrac
 t predicates. This logic reasons about a module's implementation using sep
 aration logic with permissions\, and provide abstract specifications for u
 se by client programs using concurrent abstract predicates. I will illustr
 ate this proof system with the example of a set module.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR