Succinct Representation of Concurrent Trace Sets

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.

Joint work with: Ashutosh Gupta, Tom Henzinger, Arjun Radhakrishna and Thorsten Tarrach.

Speaker biography

Roopsha Samanta is currently a postdoctoral researcher in Thomas A. Henzinger's group at the Institute of Science and Technology Austria (IST Austria).  She completed her PhD at the University of Texas at Austin in 2013.  Her supervisors were E. Allen Emerson and Vijay K. Garg.  Her research interests are program analysis, verification, repair and synthesis, quantitative reasoning, and automata theory.