BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Owicki-Gries\, Thread-Modular Model-Checking\, Cartesian Abstracti
 on - Alexander Malkis
DTSTART:20091020T120000Z
DTEND:20091020T130000Z
UID:TALK19686@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:We examine three different approaches to verification of multi
 threaded programs:\n* the Owicki-Gries annotation together with a proof ru
 le system\n* thread-modular model-checking by Flanagan and Qadeer\n* abstr
 act interpretation with a form of Cartesian abstraction\, described by the
  speaker.\n\nWe show that all three methods have the same precision. We ex
 amine a way to increase the precision\, up to completeness\, which does no
 t require auxiliary variables. We show polynomial time of the refined meth
 od on a practically interested program class.\n\nSpeaker's Bio:\nAlexander
  Malkis has obtained his diploma from Saarbrücken\, Germany\, for a work 
 on combinatorics of polyedges. At MPII and in Freiburg he was working on v
 erification of multithreaded programs under the supervision of Prof. Dr. A
 ndreas Podelski. Till the 20th of November\, he is interning at MSRC. More
  information about the speaker can be found at http://swt.informatik.uni-f
 reiburg.de/~alexmalk.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR