---
_id: '1011'
abstract:
- lang: eng
  text: Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly
    equivalent, are standard models for interprocedural analysis. Yet RSMs are more
    convenient as they (a) explicitly model function calls and returns, and (b) specify
    many natural parameters for algorithmic analysis, e.g., the number of entries
    and exits. We consider a general framework where RSM transitions are labeled from
    a semiring and path properties are algebraic with semiring operations, which can
    model, e.g., interprocedural reachability and dataflow analysis problems. Our
    main contributions are new algorithms for several fundamental problems. As compared
    to a direct translation of RSMs to PDSs and the best-known existing bounds of
    PDSs, our analysis algorithm improves the complexity for finite-height semirings
    (that subsumes reachability and standard dataflow properties). We further consider
    the problem of extracting distance values from the representation structures computed
    by our algorithm, and give efficient algorithms that distinguish the complexity
    of a one-time preprocessing from the complexity of each individual query. Another
    advantage of our algorithm is that our improvements carry over to the concurrent
    setting, where we improve the bestknown complexity for the context-bounded analysis
    of concurrent RSMs. Finally, we provide a prototype implementation that gives
    a significant speed-up on several benchmarks from the SLAM/SDV project.
alternative_title:
- LNCS
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: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
- first_name: Samarth
  full_name: Mishra, Samarth
  last_name: Mishra
- 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, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted
    recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:<a
    href="https://doi.org/10.1007/978-3-662-54434-1_11">10.1007/978-3-662-54434-1_11</a>'
  apa: 'Chatterjee, K., Kragl, B., Mishra, S., &#38; Pavlogiannis, A. (2017). Faster
    algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201,
    pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala,
    Sweden: Springer. <a href="https://doi.org/10.1007/978-3-662-54434-1_11">https://doi.org/10.1007/978-3-662-54434-1_11</a>'
  chicago: Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis.
    “Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok
    Yang, 10201:287–313. Springer, 2017. <a href="https://doi.org/10.1007/978-3-662-54434-1_11">https://doi.org/10.1007/978-3-662-54434-1_11</a>.
  ieee: 'K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms
    for weighted recursive state machines,” presented at the ESOP: European Symposium
    on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.'
  ista: 'Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms
    for weighted recursive state machines. ESOP: European Symposium on Programming,
    LNCS, vol. 10201, 287–313.'
  mla: Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Weighted Recursive
    State Machines</i>. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313,
    doi:<a href="https://doi.org/10.1007/978-3-662-54434-1_11">10.1007/978-3-662-54434-1_11</a>.
  short: K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.),
    Springer, 2017, pp. 287–313.
conference:
  end_date: 2017-04-29
  location: Uppsala, Sweden
  name: 'ESOP: European Symposium on Programming'
  start_date: 2017-04-22
date_created: 2018-12-11T11:49:41Z
date_published: 2017-03-19T00:00:00Z
date_updated: 2025-06-04T08:09:18Z
day: '19'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-54434-1_11
ec_funded: 1
editor:
- first_name: Hongseok
  full_name: Yang, Hongseok
  last_name: Yang
external_id:
  arxiv:
  - '1701.04914'
  isi:
  - '000681702400011'
intvolume: '     10201'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1701.04914
month: '03'
oa: 1
oa_version: Submitted Version
page: 287 - 313
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
publist_id: '6384'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for weighted recursive state machines
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10201
year: '2017'
...