---
res:
  bibo_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 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.\r\n\r\nWe 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.\r\n\r\nIn the first case study, we present an algorithm for inferring
    missing synchronization from an HB-Formula representing correct interleavings
    of a given trace. The algorithm applies rules to rewrite specific patterns in
    the HB-Formula into locks, barriers, and wait-notify constructs. In the second
    case study, we use an HB-Formula representing incorrect interleavings for bug
    summarization. While the HB-Formula itself is a concise counterexample summary,
    we present additional inference rules to help identify specific concurrency bugs
    such as data races, define-use order violations, and two-stage access bugs. In
    the final case study, we present a novel predicate learning procedure that uses
    HB-Formulas representing abstract counterexamples to accelerate counterexample-guided
    abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure
    refines the abstraction to eliminate multiple spurious abstract counterexamples
    drawn from the HB-Formula.@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Ashutosh
      foaf_name: Gupta, Ashutosh
      foaf_surname: Gupta
      foaf_workInfoHomepage: http://www.librecat.org/personId=335E5684-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Arjun
      foaf_name: Radhakrishna, Arjun
      foaf_surname: Radhakrishna
      foaf_workInfoHomepage: http://www.librecat.org/personId=3B51CAC4-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Roopsha
      foaf_name: Samanta, Roopsha
      foaf_surname: Samanta
      foaf_workInfoHomepage: http://www.librecat.org/personId=3D2AAC08-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Thorsten
      foaf_name: Tarrach, Thorsten
      foaf_surname: Tarrach
      foaf_workInfoHomepage: http://www.librecat.org/personId=3D6E8F2C-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0003-4409-8487
  bibo_doi: 10.1145/2676726.2677008
  dct_date: 2015^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/978-1-4503-3300-9
  dct_language: eng
  dct_publisher: ACM@
  dct_title: Succinct representation of concurrent trace sets@
...