---
res:
bibo_abstract:
- 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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Chatterjee, Krishnendu
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Bernhard
foaf_name: Kragl, Bernhard
foaf_surname: Kragl
foaf_workInfoHomepage: http://www.librecat.org/personId=320FC952-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0001-7745-9117
- foaf_Person:
foaf_givenName: Samarth
foaf_name: Mishra, Samarth
foaf_surname: Mishra
- foaf_Person:
foaf_givenName: Andreas
foaf_name: Pavlogiannis, Andreas
foaf_surname: Pavlogiannis
foaf_workInfoHomepage: http://www.librecat.org/personId=49704004-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-8943-0722
bibo_doi: 10.1007/978-3-662-54434-1_11
bibo_volume: 10201
dct_date: 2017^xs_gYear
dct_isPartOf:
- http://id.crossref.org/issn/03029743
dct_language: eng
dct_publisher: Springer@
dct_title: Faster algorithms for weighted recursive state machines@
...