Computer-aided Concurrent Programming using Concurrent Trace Sets

Add to your list(s) Download to your calendar using vCal

• Roopsha Samanta, IST Austria
• Tuesday 08 September 2015, 10:30-11:30
• Small Lecture Theatre, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

In this talk, I will first present a method and a tool TARA for generating succinct representations of sets of concurrent traces. In our 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 events. Our trace set representations can drive diverse verification, fault localization, 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.

I will present the use of TARA for synchronization synthesis from explicit specifications such as assertions. I will then present a new framework and tool LISS for synchronization synthesis from implicit specifications. The LISS framework is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation and synchronization inference rules from TARA . We have used TARA and LISS for device driver programming with promising results.

————————- This work appears in POPL 2015 and CAV 2015 , and is joint work with Pavol Cerny, Ed Clarke, Ashutosh Gupta, Tom Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small Lecture Theatre, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.