Succinct Representation of Concurrent Trace Sets

2 years 11 months ago
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 HB-formulas that are Boolean combinations of happens-before constraints between events. To generate a representation of incorrect interleavings, our method iteratively explores interleavings that violate the specification and gathers generalizations of the discovered interleavings into an HB-formula; its complement yields a representation of correct interleavings. 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 summarizad abstraction refinement based verification. In each case study, our initial experimental results have been promising. In the ...
Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakr
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where POPL
Authors Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta, Thorsten Tarrach
Comments (0)