Succinct Representation of Concurrent Trace Sets

RiSE will host a talk by Roopsha Samanta on February 19, 2015.

ABSTRACT

We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as Boolean combinations of happens-before ordering constraints between events. We claim that our trace set representations can drive diverse verification, fault localization, repair, and synthesis techniques for concurrent programs. We demonstrate this by using our tool in three case studies involving synchronization synthesis, bug summarization, and abstraction refinement based verification. In each case study, our initial experimental results have been promising.