Article

On the analysis of interacting pushdown systems

Authors:

Aarti GuptaAuthors Info & Claims

POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 303 - 314

https://doi.org/10.1145/1190216.1190262

Published: 17 January 2007 Publication History

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.

References

[1]

A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, LNCS 1243, pages 135--150, 1997.]]

Digital Library

[2]

A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejcek. Reachability analysis of multithreaded software with asynchronous communica-tion. In FSTTCS, 2005.]]

Digital Library

[3]

A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. In IJFCS, volume 14(4), pages 551--, 2003.]]

[4]

A. Bouajjani, M. Olm, and T. Touili. Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems. In CONCUR, 2005.]]

Digital Library

[5]

S. Chaki, E. Clarke, N. Kidd, T.Reps, and T.Touili. Verifying concurrent message-passing c programs with recursive calls. In TACAS, 2006.]]

Digital Library

[6]

E. A. Emerson. Temporal and Modal Logic. In Handbook of Theoretical Computer Science, Volume B, pages 997--1072, 1998.]]

Digital Library

[7]

E.A. Emerson and V. Kahlon. Model checking guarded protocols. In LICS, 2003.]]

[8]

J. Esparza and A. Podelski. Efficient Algorithms for pre and post on Interprocedural Parallel Flow Graphs. In POPL, 2000.]]

Digital Library

[9]

V. Kahlon and A. Gupta. An Automata-Theoretic Approach for Model Checking Threads for LTL Properties. In LICS, 2006.]]

Digital Library

[10]

V. Kahlon, F. Ivančić, and A. Gupta. Reasoning about threads communicating via locks. In CAV, 2005.]]

Digital Library

[11]

A. Lal, G. Balakrishnan, and T. Reps. Extended weighted pushdown systems. In CAV, 2005.]]

[12]

D. Lugiez and Ph. Schnoebelen. The Regular Viewpoint on PA-Processes. In Theor. Comput. Sci., volume 274(1--2), 2002.]]

Digital Library

[13]

S. Qadeer, S. K. Rajamani, and J. Rehof. Summarizing procedures in concurrent programs. In POPL, pages 245--255, 2004.]]

Digital Library

[14]

S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS, 2005.]]

Digital Library

[15]

G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. In ACM Trans. Program. Lang. Syst., volume 22(2), pages 416--430, 2000.]]

Digital Library

[16]

T. W. Reps, S. Schwoon, S. Jha, and D. Melski. Weighted pushdown systems and their application to interprocedural dataflow analysis. In Science of Computer Programming, volume 58(1--2), 2005.]]

Digital Library

[17]

I. Walukeiwicz. Model checking ctl properties of pushdown systems. In FSTTCS, LNCS 1974, pages 127--138, 2000.]]

Digital Library

Cited By

Liu PWahl TReps T(2020)Interprocedural Context-Unbounded Program Analysis Using Observation SequencesACM Transactions on Programming Languages and Systems10.1145/341858342:4(1-34)Online publication date: 7-Dec-2020
https://dl.acm.org/doi/10.1145/3418583
Liu PWahl T(2018)CUBA: interprocedural Context-UnBounded Analysis of concurrent programsACM SIGPLAN Notices10.1145/3296979.319241953:4(105-119)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192419
Liu PWahl TFoster JGrossman D(2018)CUBA: interprocedural Context-UnBounded Analysis of concurrent programsProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192419(105-119)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192419
Show More Cited By

Index Terms

On the analysis of interacting pushdown systems
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

On the analysis of interacting pushdown systems
Proceedings of the 2007 POPL Conference

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 ...
Model checking dynamic pushdown networks
Abstract
A dynamic pushdown network (DPN) is a set of pushdown systems (PDSs) where each process can dynamically create new instances of PDSs. DPNs are a natural model of multi-threaded programs with (possibly recursive) procedure calls and thread ... $_{}$
Pushdown module checking

Model checking is a useful method to verify automatically the correctness of a system with respect to a desired behavior, by checking whether a mathematical model of the system satisfies a formal specification of this behavior. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2007

400 pages

ISBN:1595935754

DOI:10.1145/1190216

General Chair:
Martin Hofmann
Ludwig-Maximilians U, Munich, Germany
,
Program Chair:
Matthias Felleisen
Northeastern University, Boston MA

ACM SIGPLAN Notices Volume 42, Issue 1
Proceedings of the 2007 POPL Conference
January 2007
379 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1190215
Issue’s Table of Contents

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 January 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL07

Sponsor:

POPL07: The 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 17 - 19, 2007

Nice, France

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

37
Total Citations
View Citations
507
Total Downloads

Downloads (Last 12 months)14
Downloads (Last 6 weeks)4

Reflects downloads up to 27 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liu PWahl TReps T(2020)Interprocedural Context-Unbounded Program Analysis Using Observation SequencesACM Transactions on Programming Languages and Systems10.1145/341858342:4(1-34)Online publication date: 7-Dec-2020
https://dl.acm.org/doi/10.1145/3418583
Liu PWahl T(2018)CUBA: interprocedural Context-UnBounded Analysis of concurrent programsACM SIGPLAN Notices10.1145/3296979.319241953:4(105-119)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192419
Liu PWahl TFoster JGrossman D(2018)CUBA: interprocedural Context-UnBounded Analysis of concurrent programsProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192419(105-119)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192419
Nguyen HTouili T(2018)CARET Analysis of Multithreaded ProgramsLogic-Based Program Synthesis and Transformation10.1007/978-3-319-94460-9_5(73-90)Online publication date: 10-Jul-2018
https://doi.org/10.1007/978-3-319-94460-9_5
Gupta AKahlon VQadeer STouili T(2018)Model Checking Concurrent ProgramsHandbook of Model Checking10.1007/978-3-319-10575-8_18(573-611)Online publication date: 19-May-2018
https://doi.org/10.1007/978-3-319-10575-8_18
Song FTouili T(2015)Model checking dynamic pushdown networksFormal Aspects of Computing10.1007/s00165-014-0330-y27:2(397-421)Online publication date: 1-Mar-2015
https://dl.acm.org/doi/10.1007/s00165-014-0330-y
Esparza JGanty PPoch T(2014)Pattern-Based Verification for Multithreaded ProgramsACM Transactions on Programming Languages and Systems10.1145/262964436:3(1-29)Online publication date: 15-Sep-2014
https://dl.acm.org/doi/10.1145/2629644
Song FTouili T(2013)Model Checking Dynamic Pushdown NetworksProceedings of the 11th Asian Symposium on Programming Languages and Systems - Volume 830110.1007/978-3-319-03542-0_3(33-49)Online publication date: 9-Dec-2013
https://dl.acm.org/doi/10.1007/978-3-319-03542-0_3
Long ZCalin GMajumdar RMeyer R(2012)Language-Theoretic abstraction refinementProceedings of the 15th international conference on Fundamental Approaches to Software Engineering10.1007/978-3-642-28872-2_25(362-376)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28872-2_25
Kidd NReps TDolby JVaziri M(2011)Finding concurrency-related bugs using random isolationInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3220897.322109513:6(495-518)Online publication date: 1-Nov-2011
https://dl.acm.org/doi/10.5555/3220897.3221095
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents