Skip to main content
SpringerLink
Log in

Weighted Pushdown Systems and Their Application to Interprocedural Dataflow Analysis

  • Conference paper
  • First Online:
Static Analysis (SAS 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2694))

Included in the following conference series:

Abstract

Recently, pushdown systems (PDSs) have been extended to weighted PDSs, in which each transition is labeled with a value, and the goal is to determine the meet-over-all-paths value (for paths that meet a certain criterion). This paper shows how weighted PDSs yield new algorithms for certain classes of interprocedural dataflow-analysis problems.

Supported by ONR contract N00014-01-1-0708.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A.V. Aho, R. Sethi, and J.D. Ullman. Compilers: Principles, Techniques and Tools. Addison-Wesley, 1985.

    Google Scholar 

  2. F. Bancilhon, D. Maier, Y. Sagiv, and J. Ullman. Magic sets and other strange ways to implement logic programs. In Proceedings of the Fifth ACM Symposium on Principles of Database Systems, New York, NY, 1986. ACM Press.

    Google Scholar 

  3. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model checking. In Proc. CONCUR, volume 1243 of Lec. Notes in Comp. Sci., pages 135–150. Springer-Verlag, 1997.

    MathSciNet  Google Scholar 

  4. A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. In Proc. Symp. on Princ. of Prog. Lang., pages 62–73, 2003.

    Google Scholar 

  5. H. Chen and D. Wagner. MOPS: An infrastructure for examining security properties of software. In Conf. on Comp. and Commun. Sec., November 2002.

    Google Scholar 

  6. P. Cousot and R. Cousot. Temporal abstract interpretation. In Symp. on Princ. of Prog. Lang., pages 12–25, 2000.

    Google Scholar 

  7. E. Duesterwald, R. Gupta, and M.L. Soffa. Demand-driven computation of interprocedural data flow. In Symp. on Princ. of Prog. Lang., pages 37–48, New York, NY, 1995. ACM Press.

    Google Scholar 

  8. J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Proc. Computer-Aided Verif., volume 1855 of Lec. Notes in Comp. Sci., pages 232–247, July 2000.

    Article  Google Scholar 

  9. J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural data-flow analysis. In Proceedings of FoSSaCS’99, volume 1578 of LNCS, pages 14–30. Springer, 1999.

    Google Scholar 

  10. J. Esparza, A. Kučera, and S. Schwoon. Model-checking LTL with regular valuations for pushdown systems. In Proceedings of TACAS’01, volume 2031 of LNCS, pages 306–339. Springer, 2001.

    Google Scholar 

  11. S. Horwitz, T. Reps, and M. Sagiv. Demand interprocedural dataflow analysis. In Proceedings of the Third ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 104–115, New York, NY, October 1995. ACM Press.

    Google Scholar 

  12. T. Jensen, D. Le Metayer, and T. Thorn. Verification of control flow based security properties. In 1999 IEEE Symposium on Security and Privacy, May 1999.

    Google Scholar 

  13. S. Jha and T. Reps. Analysis of SPKI/SDSI certificates using model checking. In IEEE Comp. Sec. Found. Workshop (CSFW). IEEE Computer Society Press, 2002.

    Google Scholar 

  14. J. Knoop and B. Steffen. The interprocedural coincidence theorem. In Int. Conf. on Comp. Construct., pages 125–140, 1992.

    Google Scholar 

  15. U. Moencke and R. Wilhelm. Grammar flow analysis. In H. Alblas and B. Melichar, editors, Attribute Grammars, Applications and Systems, volume 545 of Lec. Notes in Comp. Sci., pages 151–186, Prague, Czechoslovakia, June 1991. Springer-Verlag.

    Google Scholar 

  16. M. Müller-Olm and H. Seidl. Computing interprocedurally valid relations in affine programs. Tech. rep., Comp. Sci. Dept., Univ. of Trier, Trier, Ger., January 2003.

    Google Scholar 

  17. G. Ramalingam. Bounded Incremental Computation, volume 1089 of Lec. Notes in Comp. Sci. Springer-Verlag, 1996.

    Google Scholar 

  18. T. Reps. Demand interprocedural program analysis using logic databases. In R. Ramakrishnan, editor, Applications of Logic Databases. Kluwer Academic Publishers, 1994.

    Google Scholar 

  19. T. Reps. Solving demand versions of interprocedural analysis problems. In P. Fritzson, editor, Proceedings of the Fifth International Conference on Compiler Construction, volume 786 of Lec. Notes in Comp. Sci., pages 389–403, Edinburgh, Scotland, April 1994. Springer-Verlag.

    Google Scholar 

  20. T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Symp. on Princ. of Prog. Lang., pages 49–61, New York, NY, 1995. ACM Press.

    Google Scholar 

  21. T. Reps, M. Sagiv, and S. Horwitz. Interprocedural dataflow analysis via graph reachability. Tech. Rep. TR 94-14, Datalogisk Institut, Univ. of Copenhagen, 1994. Available at http://www.cs.wisc.edu/wpis/papers/diku-tr94-14.ps.

    Google Scholar 

  22. M. Sagiv, T. Reps, and S. Horwitz. Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comp. Sci., 167:131–170, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  23. D. Schmidt. Data-flowa nalysis is model checking of abstract interpretations. In Symp. on Princ. of Prog. Lang., pages 38–48, New York, NY, January 1998. ACM Press.

    Google Scholar 

  24. S. Schwoon. WPDS — a library for Weighted Pushdown Systems, 2003. Available from http://www7.in.tum.de/~schwoon/moped/#wpds.

    Google Scholar 

  25. S. Schwoon, S. Jha, T. Reps, and S. Stubblebine. On generalized authorization problems. In Comp. Sec. Found. Workshop, Wash., DC, 2003. IEEE Comp. Soc.

    Google Scholar 

  26. M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 7, pages 189–234. Prentice-Hall, Englewood Cliffs, NJ, 1981.

    Google Scholar 

  27. B. Steffen. Data flow analysis as model checking. In Int. Conf. on Theor. Aspects of Comp. Softw., volume 526 of Lec. Notes in Comp. Sci., pages 346–365. Springer-Verlag, 1991.

    Google Scholar 

  28. B. Steffen. Generating data flow analysis algorithms from modal specifications. Sci. of Comp. Prog., 21(2):115–139, 1993.

    Article  MATH  Google Scholar 

  29. D.S. Warren. Memoing for logic programs. Communications of the ACM, 35(3):93–111, March 1992.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Comp. Sci. Dept., University of Wisconsin, USA

    Thomas Reps & Somesh Jha

  2. Fakultät Inf., Universität Stuttgart, Stuttgart

    Stefan Schwoon

Authors
  1. Thomas Reps
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Schwoon
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Somesh Jha
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. École Polytechnique, STIX, 91128, Palaiseau cedex, France

    Radhia Cousot

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Reps, T., Schwoon, S., Jha, S. (2003). Weighted Pushdown Systems and Their Application to Interprocedural Dataflow Analysis. In: Cousot, R. (eds) Static Analysis. SAS 2003. Lecture Notes in Computer Science, vol 2694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44898-5_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-44898-5_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40325-8

  • Online ISBN: 978-3-540-44898-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation