University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Computer-aided Concurrent Programming using Concurrent Trace Sets

Computer-aided Concurrent Programming using Concurrent Trace Sets

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity