---
_id: '7158'
abstract:
- lang: eng
  text: "Interprocedural analysis is at the heart of numerous applications in programming
    languages, such as alias analysis, constant propagation, and so on. Recursive
    state machines (RSMs) are standard models for interprocedural analysis. We consider
    a general framework with RSMs where the transitions are labeled from a semiring
    and path properties are algebraic with semiring operations. RSMs with algebraic
    path properties can model interprocedural dataflow analysis problems, the shortest
    path problem, the most probable path problem, and so on. The traditional algorithms
    for interprocedural analysis focus on path properties where the starting point
    is fixed as the entry point of a specific method. In this work, we consider possible
    multiple queries as required in many applications such as in alias analysis. The
    study of multiple queries allows us to bring in an important algorithmic distinction
    between the resource usage of the one-time preprocessing vs for each individual
    query. The second aspect we consider is that the control flow graphs for most
    programs have constant treewidth.\r\n\r\nOur main contributions are simple and
    implementable algorithms that support multiple queries for algebraic path properties
    for RSMs that have constant treewidth. Our theoretical results show that our algorithms
    have small additional one-time preprocessing but can answer subsequent queries
    significantly faster as compared to the current algorithmic solutions for interprocedural
    dataflow analysis. We have also implemented our algorithms and evaluated their
    performance for performing on-demand interprocedural dataflow analysis on various
    domains, such as for live variable analysis and reaching definitions, on a standard
    benchmark set. Our experimental results align with our theoretical statements
    and show that after a lightweight preprocessing, on-demand queries are answered
    much faster than the standard existing algorithmic approaches.\r\n"
article_number: '23'
article_processing_charge: No
article_type: original
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
  full_name: Goharshady, Amir Kafshdar
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
- first_name: Prateesh
  full_name: Goyal, Prateesh
  last_name: Goyal
- first_name: Rasmus
  full_name: Ibsen-Jensen, Rasmus
  id: 3B699956-F248-11E8-B48F-1D18A9856A87
  last_name: Ibsen-Jensen
  orcid: 0000-0003-4783-0389
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
citation:
  ama: Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. Faster
    algorithms for dynamic algebraic queries in basic RSMs with constant treewidth.
    <i>ACM Transactions on Programming Languages and Systems</i>. 2019;41(4). doi:<a
    href="https://doi.org/10.1145/3363525">10.1145/3363525</a>
  apa: Chatterjee, K., Goharshady, A. K., Goyal, P., Ibsen-Jensen, R., &#38; Pavlogiannis,
    A. (2019). Faster algorithms for dynamic algebraic queries in basic RSMs with
    constant treewidth. <i>ACM Transactions on Programming Languages and Systems</i>.
    ACM. <a href="https://doi.org/10.1145/3363525">https://doi.org/10.1145/3363525</a>
  chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Prateesh Goyal, Rasmus
    Ibsen-Jensen, and Andreas Pavlogiannis. “Faster Algorithms for Dynamic Algebraic
    Queries in Basic RSMs with Constant Treewidth.” <i>ACM Transactions on Programming
    Languages and Systems</i>. ACM, 2019. <a href="https://doi.org/10.1145/3363525">https://doi.org/10.1145/3363525</a>.
  ieee: K. Chatterjee, A. K. Goharshady, P. Goyal, R. Ibsen-Jensen, and A. Pavlogiannis,
    “Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth,”
    <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4.
    ACM, 2019.
  ista: Chatterjee K, Goharshady AK, Goyal P, Ibsen-Jensen R, Pavlogiannis A. 2019.
    Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth.
    ACM Transactions on Programming Languages and Systems. 41(4), 23.
  mla: Chatterjee, Krishnendu, et al. “Faster Algorithms for Dynamic Algebraic Queries
    in Basic RSMs with Constant Treewidth.” <i>ACM Transactions on Programming Languages
    and Systems</i>, vol. 41, no. 4, 23, ACM, 2019, doi:<a href="https://doi.org/10.1145/3363525">10.1145/3363525</a>.
  short: K. Chatterjee, A.K. Goharshady, P. Goyal, R. Ibsen-Jensen, A. Pavlogiannis,
    ACM Transactions on Programming Languages and Systems 41 (2019).
date_created: 2019-12-09T08:33:33Z
date_published: 2019-11-01T00:00:00Z
date_updated: 2024-03-25T23:30:19Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3363525
ec_funded: 1
external_id:
  isi:
  - '000564108400004'
file:
- access_level: open_access
  checksum: 291cc86a07bd010d4815e177dac57b70
  content_type: application/pdf
  creator: dernst
  date_created: 2020-10-08T12:58:10Z
  date_updated: 2020-10-08T12:58:10Z
  file_id: '8632'
  file_name: 2019_ACMTransactions_Chatterjee.pdf
  file_size: 667357
  relation: main_file
  success: 1
file_date_updated: 2020-10-08T12:58:10Z
has_accepted_license: '1'
intvolume: '        41'
isi: 1
issue: '4'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Submitted Version
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: ACM Transactions on Programming Languages and Systems
publication_identifier:
  issn:
  - 0164-0925
publication_status: published
publisher: ACM
quality_controlled: '1'
related_material:
  record:
  - id: '8934'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Faster algorithms for dynamic algebraic queries in basic RSMs with constant
  treewidth
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 41
year: '2019'
...
---
_id: '5993'
abstract:
- lang: eng
  text: 'In this article, we consider the termination problem of probabilistic programs
    with real-valued variables. Thequestions concerned are: qualitative ones that
    ask (i) whether the program terminates with probability 1(almost-sure termination)
    and (ii) whether the expected termination time is finite (finite termination);
    andquantitative ones that ask (i) to approximate the expected termination time
    (expectation problem) and (ii) tocompute a boundBsuch that the probability not
    to terminate afterBsteps decreases exponentially (con-centration problem). To
    solve these questions, we utilize the notion of ranking supermartingales, which
    isa powerful approach for proving termination of probabilistic programs. In detail,
    we focus on algorithmicsynthesis of linear ranking-supermartingales over affine
    probabilistic programs (Apps) with both angelic anddemonic non-determinism. An
    important subclass of Apps is LRApp which is defined as the class of all Appsover
    which a linear ranking-supermartingale exists.Our main contributions are as follows.
    Firstly, we show that the membership problem of LRApp (i) canbe decided in polynomial
    time for Apps with at most demonic non-determinism, and (ii) isNP-hard and inPSPACEfor
    Apps with angelic non-determinism. Moreover, theNP-hardness result holds already
    for Appswithout probability and demonic non-determinism. Secondly, we show that
    the concentration problem overLRApp can be solved in the same complexity as for
    the membership problem of LRApp. Finally, we show thatthe expectation problem
    over LRApp can be solved in2EXPTIMEand isPSPACE-hard even for Apps withoutprobability
    and non-determinism (i.e., deterministic programs). Our experimental results demonstrate
    theeffectiveness of our approach to answer the qualitative and quantitative questions
    over Apps with at mostdemonic non-determinism.'
article_number: '7'
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Hongfei
  full_name: Fu, Hongfei
  id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
  last_name: Fu
- first_name: Petr
  full_name: Novotný, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotný
- first_name: Rouzbeh
  full_name: Hasheminezhad, Rouzbeh
  last_name: Hasheminezhad
citation:
  ama: Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative
    and quantitative termination problems for affine probabilistic programs. <i>ACM
    Transactions on Programming Languages and Systems</i>. 2018;40(2). doi:<a href="https://doi.org/10.1145/3174800">10.1145/3174800</a>
  apa: Chatterjee, K., Fu, H., Novotný, P., &#38; Hasheminezhad, R. (2018). Algorithmic
    analysis of qualitative and quantitative termination problems for affine probabilistic
    programs. <i>ACM Transactions on Programming Languages and Systems</i>. Association
    for Computing Machinery (ACM). <a href="https://doi.org/10.1145/3174800">https://doi.org/10.1145/3174800</a>
  chicago: Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad.
    “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for
    Affine Probabilistic Programs.” <i>ACM Transactions on Programming Languages and
    Systems</i>. Association for Computing Machinery (ACM), 2018. <a href="https://doi.org/10.1145/3174800">https://doi.org/10.1145/3174800</a>.
  ieee: K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis
    of qualitative and quantitative termination problems for affine probabilistic
    programs,” <i>ACM Transactions on Programming Languages and Systems</i>, vol.
    40, no. 2. Association for Computing Machinery (ACM), 2018.
  ista: Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2018. Algorithmic analysis
    of qualitative and quantitative termination problems for affine probabilistic
    programs. ACM Transactions on Programming Languages and Systems. 40(2), 7.
  mla: Chatterjee, Krishnendu, et al. “Algorithmic Analysis of Qualitative and Quantitative
    Termination Problems for Affine Probabilistic Programs.” <i>ACM Transactions on
    Programming Languages and Systems</i>, vol. 40, no. 2, 7, Association for Computing
    Machinery (ACM), 2018, doi:<a href="https://doi.org/10.1145/3174800">10.1145/3174800</a>.
  short: K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, ACM Transactions on Programming
    Languages and Systems 40 (2018).
date_created: 2019-02-14T12:29:10Z
date_published: 2018-06-01T00:00:00Z
date_updated: 2023-09-19T14:38:42Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3174800
ec_funded: 1
external_id:
  arxiv:
  - '1510.08517'
  isi:
  - '000434634500003'
intvolume: '        40'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1510.08517
month: '06'
oa: 1
oa_version: Submitted Version
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication: ACM Transactions on Programming Languages and Systems
publication_identifier:
  issn:
  - 0164-0925
publication_status: published
publisher: Association for Computing Machinery (ACM)
quality_controlled: '1'
related_material:
  record:
  - id: '1438'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Algorithmic analysis of qualitative and quantitative termination problems for
  affine probabilistic programs
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 40
year: '2018'
...
---
_id: '6009'
abstract:
- lang: eng
  text: "We study algorithmic questions wrt algebraic path properties in concurrent
    systems, where the transitions of the system are labeled from a complete, closed
    semiring. The algebraic path properties can model dataflow analysis problems,
    the shortest path problem, and many other natural problems that arise in program
    analysis. We consider that each component of the concurrent system is a graph
    with constant treewidth, a property satisfied by the controlflow graphs of most
    programs. We allow for multiple possible queries, which arise naturally in demand
    driven dataflow analysis. The study of multiple queries allows us to consider
    the tradeoff between the resource usage of the one-time preprocessing and for
    each individual query. The traditional approach constructs the product graph of
    all components and applies the best-known graph algorithm on the product. In this
    approach, even the answer to a single query requires the transitive closure (i.e.,
    the results of all possible queries), which provides no room for tradeoff between
    preprocessing and query time.\r\nOur main contributions are algorithms that significantly
    improve the worst-case running time of the traditional approach, and provide various
    tradeoffs depending on the number of queries. For example, in a concurrent system
    of two components, the traditional approach requires hexic time in the worst case
    for answering one query as well as computing the transitive closure, whereas we
    show that with one-time preprocessing in almost cubic time, each subsequent query
    can be answered in at most linear time, and even the transitive closure can be
    computed in almost quartic time. Furthermore, we establish conditional optimality
    results showing that the worst-case running time of our algorithms cannot be improved
    without achieving major breakthroughs in graph algorithms (i.e., improving the
    worst-case bound for the shortest path problem in general graphs). Preliminary
    experimental results show that our algorithms perform favorably on several benchmarks.\r\n"
article_number: '9'
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Rasmus
  full_name: Ibsen-Jensen, Rasmus
  id: 3B699956-F248-11E8-B48F-1D18A9856A87
  last_name: Ibsen-Jensen
  orcid: 0000-0003-4783-0389
- first_name: Amir Kafshdar
  full_name: Goharshady, Amir Kafshdar
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
citation:
  ama: Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. Algorithms for
    algebraic path properties in concurrent systems of constant treewidth components.
    <i>ACM Transactions on Programming Languages and Systems</i>. 2018;40(3). doi:<a
    href="https://doi.org/10.1145/3210257">10.1145/3210257</a>
  apa: Chatterjee, K., Ibsen-Jensen, R., Goharshady, A. K., &#38; Pavlogiannis, A.
    (2018). Algorithms for algebraic path properties in concurrent systems of constant
    treewidth components. <i>ACM Transactions on Programming Languages and Systems</i>.
    Association for Computing Machinery (ACM). <a href="https://doi.org/10.1145/3210257">https://doi.org/10.1145/3210257</a>
  chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, Amir Kafshdar Goharshady,
    and Andreas Pavlogiannis. “Algorithms for Algebraic Path Properties in Concurrent
    Systems of Constant Treewidth Components.” <i>ACM Transactions on Programming
    Languages and Systems</i>. Association for Computing Machinery (ACM), 2018. <a
    href="https://doi.org/10.1145/3210257">https://doi.org/10.1145/3210257</a>.
  ieee: K. Chatterjee, R. Ibsen-Jensen, A. K. Goharshady, and A. Pavlogiannis, “Algorithms
    for algebraic path properties in concurrent systems of constant treewidth components,”
    <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 3.
    Association for Computing Machinery (ACM), 2018.
  ista: Chatterjee K, Ibsen-Jensen R, Goharshady AK, Pavlogiannis A. 2018. Algorithms
    for algebraic path properties in concurrent systems of constant treewidth components.
    ACM Transactions on Programming Languages and Systems. 40(3), 9.
  mla: Chatterjee, Krishnendu, et al. “Algorithms for Algebraic Path Properties in
    Concurrent Systems of Constant Treewidth Components.” <i>ACM Transactions on Programming
    Languages and Systems</i>, vol. 40, no. 3, 9, Association for Computing Machinery
    (ACM), 2018, doi:<a href="https://doi.org/10.1145/3210257">10.1145/3210257</a>.
  short: K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions
    on Programming Languages and Systems 40 (2018).
date_created: 2019-02-14T14:31:52Z
date_published: 2018-08-01T00:00:00Z
date_updated: 2024-03-25T23:30:19Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3210257
ec_funded: 1
external_id:
  arxiv:
  - '1510.07565'
  isi:
  - '000444694800001'
intvolume: '        40'
isi: 1
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1510.07565
month: '08'
oa: 1
oa_version: Preprint
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: ACM Transactions on Programming Languages and Systems
publication_identifier:
  issn:
  - 0164-0925
publication_status: published
publisher: Association for Computing Machinery (ACM)
quality_controlled: '1'
related_material:
  record:
  - id: '1437'
    relation: earlier_version
    status: public
  - id: '5441'
    relation: earlier_version
    status: public
  - id: '5442'
    relation: earlier_version
    status: public
  - id: '8934'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Algorithms for algebraic path properties in concurrent systems of constant
  treewidth components
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 40
year: '2018'
...
---
_id: '4473'
abstract:
- lang: eng
  text: 'The simulation preorder on state transition systems is widely accepted as
    a useful notion of refinement, both in its own right and as an efficiently checkable
    sufficient condition for trace containment. For composite systems, due to the
    exponential explosion of the state space, there is a need for decomposing a simulation
    check of the form P ≤s Q, denoting &quot;P is simulated by Q,&quot; into simpler
    simulation checks on the components of P and Q. We present an assume-guarantee
    rule that enables such a decomposition. To the best of our knowledge, this is
    the first assume-guarantee rule that applies to a refinement relation different
    from trace containment. Our rule is circular, and its soundness proof requires
    induction on trace trees. The proof is constructive: given simulation relations
    that witness the simulation preorder between corresponding components of P and
    Q, we provide a procedure for constructing a witness relation for P ≤s Q. We also
    extend our assume-guarantee rule to account for fairness constraints on transition
    systems.'
article_processing_charge: No
article_type: original
author:
- 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: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
- first_name: Serdar
  full_name: Tasiran, Serdar
  last_name: Tasiran
citation:
  ama: Henzinger TA, Qadeer S, Rajamani S, Tasiran S. An assume-guarantee rule for
    checking simulation. <i>ACM Transactions on Programming Languages and Systems
    (TOPLAS)</i>. 2002;24(1):51-64. doi:<a href="https://doi.org/10.1145/509705.509707">10.1145/509705.509707</a>
  apa: Henzinger, T. A., Qadeer, S., Rajamani, S., &#38; Tasiran, S. (2002). An assume-guarantee
    rule for checking simulation. <i>ACM Transactions on Programming Languages and
    Systems (TOPLAS)</i>. ACM. <a href="https://doi.org/10.1145/509705.509707">https://doi.org/10.1145/509705.509707</a>
  chicago: Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran.
    “An Assume-Guarantee Rule for Checking Simulation.” <i>ACM Transactions on Programming
    Languages and Systems (TOPLAS)</i>. ACM, 2002. <a href="https://doi.org/10.1145/509705.509707">https://doi.org/10.1145/509705.509707</a>.
  ieee: T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee
    rule for checking simulation,” <i>ACM Transactions on Programming Languages and
    Systems (TOPLAS)</i>, vol. 24, no. 1. ACM, pp. 51–64, 2002.
  ista: Henzinger TA, Qadeer S, Rajamani S, Tasiran S. 2002. An assume-guarantee rule
    for checking simulation. ACM Transactions on Programming Languages and Systems
    (TOPLAS). 24(1), 51–64.
  mla: Henzinger, Thomas A., et al. “An Assume-Guarantee Rule for Checking Simulation.”
    <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 24,
    no. 1, ACM, 2002, pp. 51–64, doi:<a href="https://doi.org/10.1145/509705.509707">10.1145/509705.509707</a>.
  short: T.A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, ACM Transactions on Programming
    Languages and Systems (TOPLAS) 24 (2002) 51–64.
date_created: 2018-12-11T12:09:02Z
date_published: 2002-01-01T00:00:00Z
date_updated: 2023-06-05T07:59:47Z
day: '01'
doi: 10.1145/509705.509707
extern: '1'
intvolume: '        24'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 51 - 64
publication: ACM Transactions on Programming Languages and Systems (TOPLAS)
publication_identifier:
  issn:
  - 0164-0925
publication_status: published
publisher: ACM
publist_id: '256'
quality_controlled: '1'
scopus_import: '1'
status: public
title: An assume-guarantee rule for checking simulation
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 24
year: '2002'
...