BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Logic of Reachable Patterns in Linked Data-Structures - Greta Yo
 rsh (Tel Aviv University)
DTSTART:20070223T140000Z
DTEND:20070223T150000Z
UID:TALK6692@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:We define a new decidable logic for expressing and checking in
 variants of programs that manipulate dynamically-allocated objects via poi
 nters and destructive pointer updates. The main feature of this logic is t
 he ability to limit the neighborhood of a node that is reachable via a reg
 ular expression from a designated node. The logic is closed under boolean 
 operations (entailment\, negation) and has a finite model property. The ke
 y technical result is the proof of decidability. We show how to express pr
 econdition\, postconditions\, and loop invariants for some interesting pro
 grams. It is also possible to express properties such as disjointness of d
 ata-structures\, and low-level heap mutations. Moreover\, our logic can ex
 press properties of arbitrary data-structures and of an arbitrary number o
 f pointer fields. The latter provides a way to naturally specify postcondi
 tions that relate the fields on entry to a procedure to the fields on exit
 . Therefore\, it is possible to use the logic to automatically prove parti
 al correctness of programs performing low-level heap mutations.\n\n(Joint 
 work with Alexander Rabinovich\, Mooly Sagiv\, Antoine Meyer and Ahmed Bou
 ajjani)
LOCATION:FW11
END:VEVENT
END:VCALENDAR