On the analysis of interacting pushdown systems

10 years 10 months ago
On the analysis of interacting pushdown systems
Pushdown Systems (PDSs) has 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 thereby settling the problem.
Vineet Kahlon, Aarti Gupta
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where POPL
Authors Vineet Kahlon, Aarti Gupta
Comments (0)