TY - GEN
T1 - On the analysis of interacting pushdown systems
AU - Gupta, Aarti
PY - 2007
Y1 - 2007
N2 - Pushdown Systems (PDSs) have become an important paradigm for program analysis. Indeed, recent work has shown a deep connection between inter-procedural dataflow analysis for sequential programs and the model checking problem for PDSs. A natural extension of this framework to the concurrent domain hinges on the, somewhat less studied, problem of model checking Interacting Pushdown Systems. In this paper, we therefore focus on the model checking of Interacting Pushdown Systems synchronizing via the standard primitives - locks, rendezvous and broadcasts, for rich classes of temporal properties - both linear and branching time. We formulate new algorithms for model checking interacting PDSs for important fragments of LTL and the Mu-Calculus. Additionally, we also delineate precisely the decidability boundary for each of the standard synchronization primitives.
AB - Pushdown Systems (PDSs) have become an important paradigm for program analysis. Indeed, recent work has shown a deep connection between inter-procedural dataflow analysis for sequential programs and the model checking problem for PDSs. A natural extension of this framework to the concurrent domain hinges on the, somewhat less studied, problem of model checking Interacting Pushdown Systems. In this paper, we therefore focus on the model checking of Interacting Pushdown Systems synchronizing via the standard primitives - locks, rendezvous and broadcasts, for rich classes of temporal properties - both linear and branching time. We formulate new algorithms for model checking interacting PDSs for important fragments of LTL and the Mu-Calculus. Additionally, we also delineate precisely the decidability boundary for each of the standard synchronization primitives.
KW - Concurrency
KW - Dataflow analysis
KW - LTL
KW - Model checking
KW - Mu-calculus
KW - Pushdown systems
UR - http://www.scopus.com/inward/record.url?scp=34548241752&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34548241752&partnerID=8YFLogxK
U2 - 10.1145/1190216.1190262
DO - 10.1145/1190216.1190262
M3 - Conference contribution
AN - SCOPUS:34548241752
SN - 1595935754
SN - 9781595935755
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 303
EP - 314
BT - Conference Record of POPL 2007
T2 - 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Y2 - 17 January 2007 through 19 January 2007
ER -