[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/604131.604137acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article

A generic approach to the static analysis of concurrent programs with procedures

Published: 15 January 2003 Publication History

Abstract

We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known that typical dataflow problems for this model are undecidable, because the emptiness problem for the intersection of context-free languages, which is undecidable, can be reduced to them. In this paper we propose an algebraic framework for defining abstractions (upper approximations) of context-free languages. We consider two classes of abstractions: finite-chain abstractions, which are abstractions whose domains do not contain any infinite chains, and commutative abstractions corresponding to classes of languages that contain a word if and only if they contain all its permutations. We show how to compute such approximations by combining automata theoretic techniques with algorithms for solving systems of polynomial inequations in Kleene algebras.

References

[1]
J. Blieberger, B. Burgstaller, and B. Scholz. Symbolic Data Flow Analysis for Detecting Deadlocks in Ada Tasking Programs. In Proc. of the Ada-Europe International Conference on Reliable Software Technologies, Potsdam, Germany, 2000.
[2]
A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata: Application to Model Checking. In CONCUR'97, volume 1243 of LNCS, 1997.
[3]
J. C. Corbett. Automated Formal Analysis Methods for Concurrent and Real-Time Software. PhD thesis, University of Massachusetts at Amherst. 1992.
[4]
E. Duesterwald and M. Soffa. Concurrency analysis in the presence of of procedures using a data-flow framework. In Proc. of the Symposium on Testing, Analysis, and Verification, Victoria, Canada, pages 36--48. ACM Press, 1991.
[5]
M. B. Dwyer and L. A. Clarke. Data flow analysis for verifying properties of concurrent programs. In Proceedings of the ACM SIGSOFT '94 Symposium on the Foundations of Software Engineering, pages 62--75. ACM Press, 1994.
[6]
J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithm for model checking pushdown systems. In CAV'00, volume 1885 of LNCS, 2000.
[7]
J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural data-flow analysis. In W. Thomas, editor, Proc of Foundations of Software Science and Computation Structure, FoSSaCS'99, volume 1578 of Lecture Notes in Computer Science. Springer, 1999.
[8]
J. Esparza and A. Podelski. Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In Proceedings of the 27th ACM SIGPLAN-SIGACT on Principles of Programming Languages, POPL 2000, pages 1--11. ACM Press, 2000.
[9]
M. Hopkins and D. Kozen. Parikh's Theorem in Commutative Kleene Algebra. In Proc. IEEE Conf. Logic in Computer Science (LICS'99). IEEE, 1999.
[10]
D. Lugiez and P. Schnoebelen. The Regular Viewpoint on PA-processes. In TCS, volume 274(1-2), 2002.
[11]
N. Mercouroff. An algorithm for analyzing communicating processes. In Mathematical Foundations of Programming Semantics, volume 598 of LNCS, pages 312--25, 1991.
[12]
G. Naumovich and G. Avrunin. A conservative data flow algorithm for detecting all pairs of statement that may happen in parallel. In Proceedings of the ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 24--34. ACM Press, 1998.
[13]
G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Transactions on Programming Languages and Systems (TOPLAS), 22:416--430, 2000.
[14]
M. Rinard. Analysis of multithreaded programs. In P. Cousot, editor, Proc. of the 8th International Symposium on Static Analysis, SAS 2001, volume 2126 of LNCS, 2001.
[15]
R. Taylor. A general-purpose algorithm for analyzing concurrent programs. Communications of the ACM, 26:362--376, 1983.
[16]
E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. ACM SIGPLAN Notices, 36(3):27--40, 2001.

Cited By

View all
  • (2024)Comparing semantic graph representations of source code: The case of automatic feedback on programming assignmentsComputer Science and Information Systems10.2298/CSIS230615004P21:1(117-142)Online publication date: 2024
  • (2024)Weighted Context-Free-Language Ordered Binary Decision DiagramsProceedings of the ACM on Programming Languages10.1145/36897608:OOPSLA2(1390-1419)Online publication date: 8-Oct-2024
  • (2024)Newtonian Program Analysis of Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36498228:OOPSLA1(305-333)Online publication date: 29-Apr-2024
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2003
308 pages
ISBN:1581136285
DOI:10.1145/604131
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 38, Issue 1
    January 2003
    298 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/640128
    Issue’s Table of Contents
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: 15 January 2003

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. abstraction
  2. concurrent programs with procedures
  3. kleene algebras
  4. pushdown systems
  5. static analysis
  6. verification

Qualifiers

  • Article

Conference

POPL03

Acceptance Rates

POPL '03 Paper Acceptance Rate 24 of 126 submissions, 19%;
Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)14
  • Downloads (Last 6 weeks)2
Reflects downloads up to 13 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Comparing semantic graph representations of source code: The case of automatic feedback on programming assignmentsComputer Science and Information Systems10.2298/CSIS230615004P21:1(117-142)Online publication date: 2024
  • (2024)Weighted Context-Free-Language Ordered Binary Decision DiagramsProceedings of the ACM on Programming Languages10.1145/36897608:OOPSLA2(1390-1419)Online publication date: 8-Oct-2024
  • (2024)Newtonian Program Analysis of Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36498228:OOPSLA1(305-333)Online publication date: 29-Apr-2024
  • (2024)Parikh’s Theorem Made SymbolicProceedings of the ACM on Programming Languages10.1145/36329078:POPL(1945-1977)Online publication date: 5-Jan-2024
  • (2024)Reachability Analysis of Concurrent Self-modifying CodeEngineering of Complex Computer Systems10.1007/978-3-031-66456-4_14(257-271)Online publication date: 29-Sep-2024
  • (2021)A Compositional Deadlock Detector for Android Java2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE51524.2021.9678572(955-966)Online publication date: Nov-2021
  • (2020)LTL model checking for communicating concurrent programsInnovations in Systems and Software Engineering10.1007/s11334-020-00363-6Online publication date: 3-Jun-2020
  • (2019)Refinement of path expressions for static analysisProceedings of the ACM on Programming Languages10.1145/32903583:POPL(1-29)Online publication date: 2-Jan-2019
  • (2019)Program Analyses Using Newton’s Method (Invited Paper)Networked Systems10.1007/978-3-030-05529-5_1(3-16)Online publication date: 5-Jan-2019
  • (2018)Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth ComponentsACM Transactions on Programming Languages and Systems10.1145/321025740:3(1-43)Online publication date: 5-Jul-2018
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media