Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains

  • Morten Kühnrich
  • Stefan Schwoon
  • Jiří Srba
  • Stefan Kiefer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5504)


We study generalized fixed-point equations over idempotent semirings and provide an efficient algorithm for the detection whether a sequence of Kleene’s iterations stabilizes after a finite number of steps. Previously known approaches considered only bounded semirings where there are no infinite descending chains. The main novelty of our work is that we deal with semirings without the boundedness restriction. Our study is motivated by several applications from interprocedural dataflow analysis. We demonstrate how the reachability problem for weighted pushdown automata can be reduced to solving equations in the framework mentioned above and we describe a few applications to demonstrate its usability.


Model Check Polynomial Time Algorithm Weighted Post Memory Page Descend Chain Condition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Berstel, J., Boasson, L.: Formal properties of XML grammars and languages. Acta Informatica 38(9), 649–671 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Bouajjani, A., Esparza, J.: Rewriting models of boolean programs. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 136–150. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. 4.
    Esparza, J., Kiefer, S., Luttenberger, M.: An extension of Newton’s method to ω-continuous semirings. In: Harju, T., Karhumäki, J., Lepistö, A. (eds.) DLT 2007. LNCS, vol. 4588, pp. 157–168. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Esparza, J., Kiefer, S., Luttenberger, M.: On fixed point equations over commutative semirings. In: Stephanidis, C., Pieper, M. (eds.) ERCIM Ws UI4ALL 2006. LNCS, vol. 4397, pp. 296–307. Springer, Heidelberg (2007)Google Scholar
  6. 6.
    Esparza, J., Kiefer, S., Luttenberger, M.: Newton’s method for ω-continuous semirings. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 14–26. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 489–503. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Gawlitza, T., Seidl, H.: Precise fixpoint computation through strategy iteration. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 300–315. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  9. 9.
    Hopkins, M.W., Kozen, D.: Parikh’s theorem in commutative Kleene algebra. In: Proc. LICS, pp. 394–401. IEEE, Los Alamitos (1999)Google Scholar
  10. 10.
    Jha, S., Schwoon, S., Wang, H., Reps, T.: Weighted pushdown systems and trust-management systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 1–26. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Kirkegaard, C., Møller, A.: Static Analysis for Java Servlets and JSP. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 336–352. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Kühnrich, M., Schwoon, S., Srba, J., Kiefer, S.: Interprocedural dataflow analysis over weight domains with infinite descending chains. Technical report (2009),
  13. 13.
    Kuich, W.: Semirings and Formal Power Series: Their Relevance to Formal Languages and Automata. In: Handbook of Formal Languages, ch.9, vol. 1, pp. 609–677. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  14. 14.
    Lal, A., Lim, J., Polishchuk, M., Liblit, B.: Path optimization in programs and its application to debugging. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 246–263. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Leroux, J., Sutre, G.: Accelerated data-flow analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 184–199. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  16. 16.
    Love, R.: Linux Kernel Development, 2nd edn. Novell Press (2005)Google Scholar
  17. 17.
    Minamide, Y., Tozawa, A.: XML validation for context-free grammars. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol. 4279, pp. 357–373. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)CrossRefzbMATHGoogle Scholar
  19. 19.
    Reps, T., Lal, A., Kidd, N.: Program analysis using weighted pushdown systems. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 23–51. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  20. 20.
    Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. SCP 58(1–2), 206–263 (2005)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, TU Munich (2002)Google Scholar
  22. 22.
    Sharir, M., Pnueli, A.: Two Approaches to Interprocedural Data Flow Analysis. In: Program Flow Analysis: Theory and Applications, ch.7, pp. 189–233. Prentice-Hall, Englewood Cliffs (1981)Google Scholar
  23. 23.
    Suwimonteerabuth, D., Berger, F., Schwoon, S., Esparza, J.: jMoped: A test environment for Java programs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 164–167. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  24. 24.
    Tozawa, A., Minamide, Y.: Complexity results on balanced context-free languages. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 346–360. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  25. 25.
    Woo, T.Y.C., Lam, S.S.: A semantic model for authentication protocols. In: Proc. SP, pp. 112–118. IEEE, Los Alamitos (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Morten Kühnrich
    • 2
  • Stefan Schwoon
    • 1
  • Jiří Srba
    • 2
  • Stefan Kiefer
    • 1
  1. 1.Technische Universität MünchenGarchingGermany
  2. 2.Department of Computer ScienceAalborg UniversityAalborg EastDenmark

Personalised recommendations