---
_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."
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:10.1145/2676726.2677008'
apa: 'Gupta, A., Henzinger, T. A., Radhakrishna, A., Samanta, R., & Tarrach,
T. (2015). Succinct representation of concurrent trace sets (pp. 433–444). Presented
at the POPL: Principles of Programming Languages, Mumbai, India: ACM. https://doi.org/10.1145/2676726.2677008'
chicago: Gupta, Ashutosh, Thomas A Henzinger, Arjun Radhakrishna, Roopsha Samanta,
and Thorsten Tarrach. “Succinct Representation of Concurrent Trace Sets,” 433–44.
ACM, 2015. https://doi.org/10.1145/2676726.2677008.
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. Succinct Representation of Concurrent Trace Sets.
ACM, 2015, pp. 433–44, doi:10.1145/2676726.2677008.
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: 2021-01-12T06:54:33Z
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'
...
---
_id: '1604'
abstract:
- lang: eng
text: We consider the quantitative analysis problem for interprocedural control-flow
graphs (ICFGs). The input consists of an ICFG, a positive weight function that
assigns every transition a positive integer-valued number, and a labelling of
the transitions (events) as good, bad, and neutral events. The weight function
assigns to each transition a numerical value that represents ameasure of how good
or bad an event is. The quantitative analysis problem asks whether there is a
run of the ICFG where the ratio of the sum of the numerical weights of good events
versus the sum of weights of bad events in the long-run is at least a given threshold
(or equivalently, to compute the maximal ratio among all valid paths in the ICFG).
The quantitative analysis problem for ICFGs can be solved in polynomial time,
and we present an efficient and practical algorithm for the problem. We show that
several problems relevant for static program analysis, such as estimating the
worst-case execution time of a program or the average energy consumption of a
mobile application, can be modeled in our framework. We have implemented our algorithm
as a tool in the Java Soot framework. We demonstrate the effectiveness of our
approach with two case studies. First, we show that our framework provides a sound
approach (no false positives) for the analysis of inefficiently-used containers.
Second, we show that our approach can also be used for static profiling of programs
which reasons about methods that are frequently invoked. Our experimental results
show that our tool scales to relatively large benchmarks, and discovers relevant
and useful information that can be used to optimize performance of the programs.
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
- first_name: Yaron
full_name: Velner, Yaron
last_name: Velner
citation:
ama: Chatterjee K, Pavlogiannis A, Velner Y. Quantitative interprocedural analysis.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 2015;50(1):539-551.
doi:10.1145/2676726.2676968
apa: 'Chatterjee, K., Pavlogiannis, A., & Velner, Y. (2015). Quantitative interprocedural
analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . Mumbai, India:
ACM. https://doi.org/10.1145/2676726.2676968'
chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. “Quantitative
Interprocedural Analysis.” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT
. ACM, 2015. https://doi.org/10.1145/2676726.2676968.
ieee: K. Chatterjee, A. Pavlogiannis, and Y. Velner, “Quantitative interprocedural
analysis,” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT , vol. 50,
no. 1. ACM, pp. 539–551, 2015.
ista: Chatterjee K, Pavlogiannis A, Velner Y. 2015. Quantitative interprocedural
analysis. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT . 50(1), 539–551.
mla: Chatterjee, Krishnendu, et al. “Quantitative Interprocedural Analysis.” Proceedings
of the 42nd Annual ACM SIGPLAN-SIGACT , vol. 50, no. 1, ACM, 2015, pp. 539–51,
doi:10.1145/2676726.2676968.
short: K. Chatterjee, A. Pavlogiannis, Y. Velner, Proceedings of the 42nd Annual
ACM SIGPLAN-SIGACT 50 (2015) 539–551.
conference:
end_date: 2015-01-17
location: Mumbai, India
name: 'SIGPLAN: Symposium on Principles of Programming Languages'
start_date: 2015-01-15
date_created: 2018-12-11T11:52:59Z
date_published: 2015-01-01T00:00:00Z
date_updated: 2023-09-07T12:01:59Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2676726.2676968
ec_funded: 1
intvolume: ' 50'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 539 - 551
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: 'Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT '
publication_identifier:
isbn:
- 978-1-4503-3300-9
publication_status: published
publisher: ACM
publist_id: '5563'
pubrep_id: '523'
quality_controlled: '1'
related_material:
record:
- id: '5445'
relation: earlier_version
status: public
- id: '821'
relation: dissertation_contains
status: public
scopus_import: 1
status: public
title: Quantitative interprocedural analysis
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 50
year: '2015'
...