BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Computer-aided Concurrent Programming using Concurrent Trace Sets 
  - Roopsha Samanta\, IST Austria
DTSTART:20150908T093000Z
DTEND:20150908T103000Z
UID:TALK60687@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:In this talk\, I will first present a method and a tool TARA f
 or generating succinct representations of sets of concurrent traces. In ou
 r work\, we focus on trace sets that contain all correct or all incorrect 
 permutations of events from a given trace. We represent such trace sets as
  Boolean combinations of happens-before ordering constraints between event
 s. Our trace set representations can drive diverse verification\, fault lo
 calization\, repair\, and synthesis techniques for concurrent programs. In
  the remainder of the talk\, I will focus on the use of our representation
  for synchronization synthesis.\n\nI will present the use of TARA for sync
 hronization synthesis from explicit specifications such as assertions. I w
 ill then present a new framework and tool LISS for synchronization synthes
 is from implicit specifications. The LISS framework is based on a finitary
  abstraction\, an algorithm for bounded language inclusion modulo an indep
 endence relation and synchronization inference rules from TARA. We have us
 ed TARA and LISS for device driver programming with\npromising results.\n\
 n-----------------\nThis work appears in POPL 2015 and CAV 2015\, and is j
 oint work with Pavol Cerny\,\nEd Clarke\, Ashutosh Gupta\, Tom Henzinger\,
  Arjun Radhakrishna\, Leonid Ryzhyk and\nThorsten Tarrach.\n
LOCATION:Small Lecture Theatre\, Microsoft Research Ltd\, 21 Station Road\
 , Cambridge\, CB1 2FB
END:VEVENT
END:VCALENDAR