Abstract
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.
The second and fourth authors are supported in part by the DFG project Algorithms for Software Model Checking. The third author is supported in part by Institute for Theoretical Computer Science, project No. 1M0545.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Berstel, J., Boasson, L.: Formal properties of XML grammars and languages. Acta Informatica 38(9), 649–671 (2002)
Bouajjani, A., Esparza, J.: Rewriting models of boolean programs. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 136–150. Springer, Heidelberg (2006)
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)
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)
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)
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)
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)
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)
Hopkins, M.W., Kozen, D.: Parikh’s theorem in commutative Kleene algebra. In: Proc. LICS, pp. 394–401. IEEE, Los Alamitos (1999)
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)
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)
Kühnrich, M., Schwoon, S., Srba, J., Kiefer, S.: Interprocedural dataflow analysis over weight domains with infinite descending chains. Technical report (2009), http://arxiv.org/abs/0901.0501
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)
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)
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)
Love, R.: Linux Kernel Development, 2nd edn. Novell Press (2005)
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)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)
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)
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)
Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, TU Munich (2002)
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)
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)
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)
Woo, T.Y.C., Lam, S.S.: A semantic model for authentication protocols. In: Proc. SP, pp. 112–118. IEEE, Los Alamitos (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kühnrich, M., Schwoon, S., Srba, J., Kiefer, S. (2009). Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains. In: de Alfaro, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2009. Lecture Notes in Computer Science, vol 5504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00596-1_31
Download citation
DOI: https://doi.org/10.1007/978-3-642-00596-1_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00595-4
Online ISBN: 978-3-642-00596-1
eBook Packages: Computer ScienceComputer Science (R0)