Abstract

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.