BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Poirot — a concurrency sleuth - Shaz Qadeer\, Microsoft Research
  Redmond
DTSTART:20111025T100000Z
DTEND:20111025T110000Z
UID:TALK34127@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Concurrent programming is difficult. The challenges are founda
 tional: unlike sequential control flow\, asynchronous control flow is diff
 icult to understand and reason about. Not surprisingly\, even expert progr
 ammers find it difficult to write concurrent software. We desperately need
  software engineering techniques and tools to move concurrent programming 
 from black art to a rigorous engineering discipline. I believe that automa
 ted tools that reduce the cognitive burden of reasoning about concurrency 
 can help tremendously in improving the productivity of concurrent programm
 ers. In collaboration with my colleagues at Microsoft Research\, I have de
 veloped Poirot (http://research.microsoft.com/en-us/projects/poirot/)\, a 
 tool for answering semantic queries about a concurrent program by statical
 ly searching over its executions. Poirot exploits sequential encodings of 
 concurrent semantics\, structural under- and over-approximations for seque
 ntial control flow\, and advances in automated theorem proving to search c
 oncurrent program executions efficiently. Poirot is being used in many dif
 ferent applications---bug detection\, program understanding\, and symbolic
  debugging. This lecture will present both a demonstration and an explanat
 ion of the techniques underlying the search engine inside Poirot.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR