---
_id: '1992'
abstract:
- lang: eng
  text: "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."
article_processing_charge: No
author:
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Arjun
  full_name: Radhakrishna, Arjun
  id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
  last_name: Radhakrishna
- first_name: Roopsha
  full_name: Samanta, Roopsha
  id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87
  last_name: Samanta
- first_name: Thorsten
  full_name: Tarrach, Thorsten
  id: 3D6E8F2C-F248-11E8-B48F-1D18A9856A87
  last_name: Tarrach
  orcid: 0000-0003-4409-8487
citation:
  ama: 'Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation
    of concurrent trace sets. In: ACM; 2015:433-444. doi:<a href="https://doi.org/10.1145/2676726.2677008">10.1145/2676726.2677008</a>'
  apa: 'Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., &#38; Tarrach,
    T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented
    at the POPL: Principles of Programming Languages, Mumbai, India: ACM. <a href="https://doi.org/10.1145/2676726.2677008">https://doi.org/10.1145/2676726.2677008</a>'
  chicago: Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta,
    and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44.
    ACM, 2015. <a href="https://doi.org/10.1145/2676726.2677008">https://doi.org/10.1145/2676726.2677008</a>.
  ieee: 'A. Gupta, T. A. Henzinger, A. Radhakrishna, R. Samanta, and T. Tarrach, “Succinct
    representation of concurrent trace sets,” presented at the POPL: Principles of
    Programming Languages, Mumbai, India, 2015, pp. 433–444.'
  ista: 'Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. 2015. Succinct
    representation of concurrent trace sets. POPL: Principles of Programming Languages,
    433–444.'
  mla: Gupta, Ashutosh, et al. <i>Succinct Representation of Concurrent Trace Sets</i>.
    ACM, 2015, pp. 433–44, doi:<a href="https://doi.org/10.1145/2676726.2677008">10.1145/2676726.2677008</a>.
  short: A. Gupta, T.A. Henzinger, A. Radhakrishna, R. Samanta, T. Tarrach, in:, ACM,
    2015, pp. 433–444.
conference:
  end_date: 2015-01-17
  location: Mumbai, India
  name: 'POPL: Principles of Programming Languages'
  start_date: 2015-01-15
date_created: 2018-12-11T11:55:05Z
date_published: 2015-01-15T00:00:00Z
date_updated: 2025-03-07T08:44:29Z
day: '15'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1145/2676726.2677008
file:
- access_level: open_access
  checksum: f0d4395b600f410a191256ac0b73af32
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:17:56Z
  date_updated: 2020-07-14T12:45:22Z
  file_id: '5314'
  file_name: IST-2015-317-v1+1_author_version.pdf
  file_size: 399462
  relation: main_file
file_date_updated: 2020-07-14T12:45:22Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 433 - 444
publication_identifier:
  isbn:
  - 978-1-4503-3300-9
publication_status: published
publisher: ACM
publist_id: '5091'
pubrep_id: '317'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Succinct representation of concurrent trace sets
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...