On the analysis of interacting pushdown systems

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationConference Record of POPL 2007
Subtitle of host publicationThe 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Papers Presented at the Symposium
Pages303-314
Number of pages12
DOIs
StatePublished - Sep 3 2007
Externally publishedYes
Event34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Nice, France
Duration: Jan 17 2007Jan 19 2007

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
CountryFrance
CityNice
Period1/17/071/19/07

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Concurrency
  • Dataflow analysis
  • LTL
  • Model checking
  • Mu-calculus
  • Pushdown systems

Fingerprint Dive into the research topics of 'On the analysis of interacting pushdown systems'. Together they form a unique fingerprint.

Cite this